1 /-
2 Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Robert Y. Lewis
5
6 -/
7
8 import data.real.cau_seq_completion
src └──────────────────────────┘
9 import data.padics.padic_norm algebra.archimedean analysis.normed_space.basic
src └────────────────────┘ └─────────────────┘ └─────────────────────────┘
10 import tactic.norm_cast
src └──────────────┘
11
12 /-!
13 # p-adic numbers
14
15 This file defines the p-adic numbers (rationals) ℚ_p as the completion of ℚ with respect to the
16 p-adic norm. We show that the p-adic norm on ℚ extends to ℚ_p, that ℚ is embedded in ℚ_p, and that
17 ℚ_p is Cauchy complete.
18
19 ## Important definitions
20
21 * `padic` : the type of p-adic numbers
22 * `padic_norm_e` : the rational valued p-adic norm on ℚ_p
23
24 ## Notation
25
26 We introduce the notation ℚ_[p] for the p-adic numbers.
27
28 ## Implementation notes
29
30 Much, but not all, of this file assumes that `p` is prime. This assumption is inferred automatically
31 by taking (prime p) as a type class argument.
32
33 We use the same concrete Cauchy sequence construction that is used to construct ℝ. ℚ_p inherits a
34 field structure from this construction. The extension of the norm on ℚ to ℚ_p is *not* analogous to
35 extending the absolute value to ℝ, and hence the proof that ℚ_p is complete is different from the
36 proof that ℝ is complete.
37
38 A small special-purpose simplification tactic, `padic_index_simp`, is used to manipulate sequence
39 indices in the proof that the norm extends.
40
41 `padic_norm_e` is the rational-valued p-adic norm on ℚ_p. To instantiate ℚ_p as a normed field, we
42 must cast this into a ℝ-valued norm. The ℝ-valued norm, using notation ∥ ∥ from normed spaces, is
43 the canonical representation of this norm.
44
45 Coercions from ℚ to ℚ_p are set up to work with the `norm_cast` tactic.
46
47 ## References
48
49 * [F. Q. Gouêva, *p-adic numbers*][gouvea1997]
50 * [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019]
51 * <https://en.wikipedia.org/wiki/P-adic_number>
52
53 ## Tags
54
55 p-adic, p adic, padic, norm, valuation, cauchy, completion, p-adic completion
56 -/
57
58 noncomputable theory
59 open_locale classical
60
61 open nat multiplicity padic_norm cau_seq cau_seq.completion metric
62
63 /-- The type of Cauchy sequences of rationals with respect to the p-adic norm. -/
64 @[reducible] def padic_seq (p : ℕ) [p.prime] := cau_seq _ (padic_norm p)
id ┴ ┴└────┘ └─────┘ └────────┘ ┴
src ┴ └────┘ └─────┘ └────────┘
typ ┴ ┴└────┘ └─────┘ └────────┘ ┴
doc └───────┘ └────┘ └────────┘
65
66 namespace padic_seq
67
68 section
69 variables {p : ℕ} [nat.prime p]
id ┴ └───────┘
src ┴ └───────┘
typ ┴ └───────┘
doc └───────┘
70
71 /-- The p-adic norm of the entries of a nonzero Cauchy sequence of rationals is eventually
72 constant. -/
73 lemma stationary {f : cau_seq ℚ (padic_norm p)} (hf : ¬ f ≈ 0) :
id └─────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ └────────┘ ┴ ┴
typ └─────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
doc ┴ └────────┘
74 ∃ N, ∀ m n, N ≤ m → N ≤ n → padic_norm p (f n) = padic_norm p (f m) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └────────┘ └────────┘
75 have ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padic_norm p (f j),
id ┴ ┴ ┴ ┴ └┘┴ ┴ └┘ ┴ ┴ └────────┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └────────┘
typ ┴ ┴ ┴ ┴ └┘┴ ┴ └┘ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └────────┘
76 from cau_seq.abv_pos_of_not_lim_zero $ not_lim_zero_of_not_congr_zero hf,
id └─────────────────────────────┘ └────────────────────────────┘ └┘
src └─────────────────────────────┘ └────────────────────────────┘
typ └─────────────────────────────┘ └────────────────────────────┘ └┘
77 let ⟨ε, hε, N1, hN1⟩ := this,
id └─┘ ┴ └┘ └┘ └─┘ └──┘
typ └─┘ ┴ └┘ └┘ └─┘ └──┘
78 ⟨N2, hN2⟩ := cau_seq.cauchy₂ f hε in
id └┘ └─┘ └─────────────┘ ┴
src └─────────────┘
typ └┘ └─┘ └─────────────┘ ┴
79 ⟨ max N1 N2,
id └─┘
src └─┘
typ └─┘
80 λ n m hn hm,
id ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘
81 have padic_norm p (f n - f m) < ε, from hN2 _ _ (max_le_iff.1 hn).2 (max_le_iff.1 hm).2,
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘┴ └┘ ┴ └────────┘┴ └┘ ┴
src └────────┘ ┴ ┴ └────────┘┴ ┴ └────────┘┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘┴ └┘ ┴ └────────┘┴ └┘ ┴
doc └────────┘
82 have padic_norm p (f n - f m) < padic_norm p (f n),
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
src └────────┘ ┴ ┴ └────────┘
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └────────┘ └────────┘
83 from lt_of_lt_of_le this $ hN1 _ (max_le_iff.1 hn).1,
id └────────────┘ └──┘ └────────┘┴ └┘ ┴
src └────────────┘ └────────┘┴ ┴
typ └────────────┘ └──┘ └────────┘┴ └┘ ┴
84 have padic_norm p (f n - f m) < max (padic_norm p (f n)) (padic_norm p (f m)),
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
src └────────┘ ┴ ┴ └─┘ └────────┘ └────────┘
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
85 from lt_max_iff.2 (or.inl this),
id └────────┘┴ └────┘ └──┘
src └────────┘┴ └────┘
typ └────────┘┴ └────┘ └──┘
86 begin
st └─────
87 by_contradiction hne,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └──┘
st ───────────────────────┘└─
88 rw ←padic_norm.neg p (f m) at hne,
id └────────────┘ ┴ ┴ ┴
src └──┘└────────────┘┴ ┴ ┴ └──────┘
typ └──┘└────────────┘┴┴┴ ┴┴┴└──────┘
doc └──┘└────────────┘┴ ┴ ┴ └──────┘
txt └──┘ ┴ ┴ ┴ └──────┘
par └──┘ ┴ ┴ ┴ └──────┘
pid └┘ ┴ ┴ ┴ ┴└─────┘
st ────────────────────────────────────┘└─
89 have hnam := add_eq_max_of_ne p hne,
id └──────────────┘ ┴ └─┘
src └───────────┘└──────────────┘┴ ┴
typ └───────────┘└──────────────┘┴┴┴└─┘
doc └───────────┘└──────────────┘┴ ┴
txt └───────────┘ ┴ ┴
par └───────────┘ ┴ ┴
pid └───────┘┴└─┘ ┴ ┴
st ──────────────────────────────────────┘└─
90 rw [padic_norm.neg, max_comm] at hnam,
id └────────────┘ └──────┘
src └──┘└────────────┘└┘└──────┘└───────┘
typ └──┘└────────────┘└┘└──────┘└───────┘
doc └──┘└────────────┘└┘ └───────┘
txt └──┘ └┘ └───────┘
par └──┘ └┘ └───────┘
pid └┘ └┘ ┴└──────┘
st ─────────────────────┘└────────┘┴└──────┘└─
91 rw ←hnam at this,
id └──┘
src └──┘ └──────┘
typ └──┘└──┘└──────┘
doc └──┘ └──────┘
txt └──┘ └──────┘
par └──┘ └──────┘
pid └┘ └──────┘
st ───────────────────┘└─
92 apply _root_.lt_irrefl _ (by simp at this; exact this)
id └──────────────┘ └──┘
src └────┘└──────────────┘└─┘ ┴└──────────┘└┘└────┘ └─
typ └────┘└──────────────┘└─┘ ┴└──────────┘└──────┘└──┘└─
doc └────┘ └─┘ ┴└──────────┘└┘└────┘ └─
txt └────┘ └─┘ ┴└──────────┘└┘└────┘ └─
par └────┘ └─┘ ┴└──────────┘└──────┘ └─
pid ┴ └─┘ └───────────────────┘ ┴└
st ───────────────────────────────┘└───────────────────────┘└─
93 end ⟩
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
94
95 /-- For all n ≥ stationary_point f hf, the p-adic norm of f n is the same. -/
96 def stationary_point {f : padic_seq p} (hf : ¬ f ≈ 0) : ℕ :=
id └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘
97 classical.some $ stationary hf
id └────────────┘ └────────┘ └┘
src └────────────┘ └────────┘
typ └────────────┘ └────────┘ └┘
doc └────────┘
98
99 lemma stationary_point_spec {f : padic_seq p} (hf : ¬ f ≈ 0) :
id └───────┘ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
100 ∀ {m n}, m ≥ stationary_point hf → n ≥ stationary_point hf →
id ┴ ┴ ┴ ┴ └──────────────┘ └┘ ┴ ┴ └──────────────┘ └┘
src ┴ └──────────────┘ ┴ └──────────────┘
typ ┴ ┴ ┴ ┴ └──────────────┘ └┘ ┴ ┴ └──────────────┘ └┘
doc └──────────────┘ └──────────────┘
101 padic_norm p (f n) = padic_norm p (f m) :=
id └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
src └────────┘ ┴ └────────┘
typ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └────────┘ └────────┘
102 classical.some_spec $ stationary hf
id └─────────────────┘ └────────┘ └┘
src └─────────────────┘ └────────┘
typ └─────────────────┘ └────────┘ └┘
doc └────────┘
103
104 /-- Since the norm of the entries of a Cauchy sequence is eventually stationary, we can lift the norm
105 to sequences. -/
106 def norm (f : padic_seq p) : ℚ :=
id └───────┘ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴
doc └───────┘ ┴
107 if hf : f ≈ 0 then 0 else padic_norm p (f (stationary_point hf))
id └┘ ┴ ┴ └────────┘ ┴ ┴ └──────────────┘ └┘
src └┘ ┴ └────────┘ └──────────────┘
typ └┘ ┴ ┴ └────────┘ ┴ ┴ └──────────────┘ └┘
doc └────────┘ └──────────────┘
108
109 lemma norm_zero_iff (f : padic_seq p) : f.norm = 0 ↔ f ≈ 0 :=
id └───────┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴
src └───────┘ └───┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴
doc └───────┘ └───┘
110 begin
st └─────
111 constructor,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
st ────────────┘└─
112 { intro h,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ───┘└─────┘└─
113 by_contradiction hf,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └─┘
st ──────────────────────┘└─
114 unfold norm at h, split_ifs at h,
src └──────────────┘ └────────────┘
typ └──────────────┘ └────────────┘
doc └──────────────┘ └────────────┘
txt └──────────────┘ └────────────┘
par └──────────────┘ └────────────┘
pid └───┘└───┘ └───┘
st ───────────────────┘└──────────────┘└─
115 apply hf,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────┘└─
116 intros ε hε,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
117 existsi stationary_point hf,
id └──────────────┘ └┘
src └──────┘└──────────────┘┴
typ └──────┘└──────────────┘┴└┘
doc └──────┘└──────────────┘┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴ ┴
st ──────────────────────────────┘└─
118 intros j hj,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
119 have heq := stationary_point_spec hf (le_refl _) hj,
id └───────────────────┘ └┘ └─────┘ └┘
src └──────────┘└───────────────────┘┴ ┴ └─────┘└──┘
typ └──────────┘└───────────────────┘┴└┘┴ └─────┘└──┘└┘
doc └──────────┘ ┴ ┴ └──┘
txt └──────────┘ ┴ ┴ └──┘
par └──────────┘ ┴ ┴ └──┘
pid └──────┘┴└─┘ ┴ ┴ └──┘
st ──────────────────────────────────────────────────────┘└─
120 simpa [h, heq] },
id ┴ └─┘
src └─────┘ └┘└─┘└┘
typ └─────┘┴└┘└─┘└┘
doc └─────┘ └┘ └┘
txt └─────┘ └┘ └┘
par └─────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ──────────────────┘└┘└
121 { intro h,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ──────────┘└─
122 simp [norm, h] }
id └──┘ ┴
src └────┘└──┘└┘ └┘
typ └────┘└──┘└┘┴└┘
doc └────┘└──┘└┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ──────────────────┘└─
123 end
st ──┘
124
125 end
126
127 section embedding
128 open cau_seq
129 variables {p : ℕ} [nat.prime p]
id ┴ └───────┘
src ┴ └───────┘
typ ┴ └───────┘
doc └───────┘
130
131 lemma equiv_zero_of_val_eq_of_equiv_zero {f g : padic_seq p}
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
doc └───────┘
132 (h : ∀ k, padic_norm p (f k) = padic_norm p (g k)) (hf : f ≈ 0) : g ≈ 0 :=
id ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ └────────┘ ┴ ┴
typ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘
133 λ ε hε, let ⟨i, hi⟩ := hf _ hε in
id ┴ └┘ └─┘ ┴ └┘ └┘
typ ┴ └┘ └─┘ ┴ └┘ └┘
134 ⟨i, λ j hj, by simpa [h] using hi _ hj⟩
id ┴ └┘ ┴ └┘ └┘
src └─────┘ └──────┘ └─┘
typ ┴ └┘ └─────┘┴└──────┘└┘└─┘└┘
doc └─────┘ └──────┘ └─┘
txt └─────┘ └──────┘ └─┘
par └─────┘ └──────┘ └─┘
pid ┴┴ ┴┴└────┘ └─┘
st └──────────────────────┘
135
136 lemma norm_nonzero_of_not_equiv_zero {f : padic_seq p} (hf : ¬ f ≈ 0) :
id └───────┘ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
137 f.norm ≠ 0 :=
id ┴└───┘ ┴
src └───┘ ┴
typ ┴└───┘ ┴
doc └───┘
138 hf ∘ f.norm_zero_iff.1
id └┘ ┴ ┴└────────────┘┴
src ┴ └────────────┘┴
typ └┘ ┴ ┴└────────────┘┴
139
140 lemma norm_eq_norm_app_of_nonzero {f : padic_seq p} (hf : ¬ f ≈ 0) :
id └───────┘ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
141 ∃ k, f.norm = padic_norm p k ∧ k ≠ 0 :=
id ┴ ┴┴ ┴└───┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ ┴ └────────┘ ┴ ┴
typ ┴ ┴┴ ┴└───┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └────────┘
142 have heq : f.norm = padic_norm p (f $ stationary_point hf), by simp [norm, hf],
id ┴└───┘ ┴ └────────┘ ┴ ┴ └──────────────┘ └┘ └──┘ └┘
src └───┘ ┴ └────────┘ └──────────────┘ └────┘└──┘└┘ ┴
typ ┴└───┘ ┴ └────────┘ ┴ ┴ └──────────────┘ └┘ └────┘└──┘└┘└┘┴
doc └───┘ └────────┘ └──────────────┘ └────┘└──┘└┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └──────────────┘
143 ⟨f $ stationary_point hf, heq,
id ┴ └──────────────┘ └┘ └─┘
src └──────────────┘ └─┘
typ ┴ └──────────────┘ └┘ └─┘
doc └──────────────┘
144 λ h, norm_nonzero_of_not_equiv_zero hf (by simpa [h] using heq)⟩
id ┴ └────────────────────────────┘ └┘ ┴ └─┘
src └────────────────────────────┘ └─────┘ └──────┘└─┘
typ ┴ └────────────────────────────┘ └┘ └─────┘┴└──────┘└─┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └──────────────────┘
145
146 lemma not_lim_zero_const_of_nonzero {q : ℚ} (hq : q ≠ 0) : ¬ lim_zero (const (padic_norm p) q) :=
id ┴ ┴ ┴ ┴ └──────┘ └───┘ └────────┘ ┴ ┴
src ┴ ┴ ┴ └──────┘ └───┘ └────────┘
typ ┴ ┴ ┴ ┴ └──────┘ └───┘ └────────┘ ┴ ┴
doc ┴ └──────┘ └───┘ └────────┘
147 λ h', hq $ const_lim_zero.1 h'
id └┘ └┘ └────────────┘┴ └┘
src └────────────┘┴
typ └┘ └┘ └────────────┘┴ └┘
148
149 lemma not_equiv_zero_const_of_nonzero {q : ℚ} (hq : q ≠ 0) : ¬ (const (padic_norm p) q) ≈ 0 :=
id ┴ ┴ ┴ ┴ └───┘ └────────┘ ┴ ┴ ┴
src ┴ ┴ ┴ └───┘ └────────┘ ┴
typ ┴ ┴ ┴ ┴ └───┘ └────────┘ ┴ ┴ ┴
doc ┴ └───┘ └────────┘
150 λ h : lim_zero (const (padic_norm p) q - 0), not_lim_zero_const_of_nonzero hq $ by simpa using h
id └──────┘ └───┘ └────────┘ ┴ ┴ ┴ └───────────────────────────┘ └┘ ┴
src └──────┘ └───┘ └────────┘ ┴ └───────────────────────────┘ └──────────┘ └
typ └──────┘ └───┘ └────────┘ ┴ ┴ ┴ └───────────────────────────┘ └┘ └──────────┘┴└
doc └──────┘ └───┘ └────────┘ └──────────┘ └
txt └──────────┘ └
par └──────────┘ └
pid ┴└────┘ └
st └──────────────
151
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
152 lemma norm_nonneg (f : padic_seq p) : f.norm ≥ 0 :=
id └───────┘ ┴ ┴└───┘ ┴
src └───────┘ └───┘ ┴
typ └───────┘ ┴ ┴└───┘ ┴
doc └───────┘ └───┘
153 if hf : f ≈ 0 then by simp [hf, norm]
id └┘ ┴ ┴ └┘ └──┘
src └┘ ┴ └────┘ └┘└──┘└┘
typ └┘ ┴ ┴ └────┘└┘└┘└──┘└┘
doc └────┘ └┘└──┘└┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st └───────────────┘
154 else by simp [norm, hf, padic_norm.nonneg]
id └──┘ └┘ └───────────────┘
src └────┘└──┘└┘ └┘└───────────────┘└─
typ └────┘└──┘└┘└┘└┘└───────────────┘└─
doc └────┘└──┘└┘ └┘└───────────────┘└─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └───────────────────────────────────
155
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
156 /-- An auxiliary lemma for manipulating sequence indices. -/
157 lemma lift_index_left_left {f : padic_seq p} (hf : ¬ f ≈ 0) (v2 v3 : ℕ) :
id └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘
158 padic_norm p (f (stationary_point hf)) =
id └────────┘ ┴ ┴ └──────────────┘ └┘ ┴
src └────────┘ └──────────────┘ ┴
typ └────────┘ ┴ ┴ └──────────────┘ └┘ ┴
doc └────────┘ └──────────────┘
159 padic_norm p (f (max (stationary_point hf) (max v2 v3))) :=
id └────────┘ ┴ ┴ └─┘ └──────────────┘ └┘ └─┘ └┘ └┘
src └────────┘ └─┘ └──────────────┘ └─┘
typ └────────┘ ┴ ┴ └─┘ └──────────────┘ └┘ └─┘ └┘ └┘
doc └────────┘ └──────────────┘
160 let i := max (stationary_point hf) (max v2 v3) in
id ┴ └─┘ └──────────────┘ └┘ └─┘ └┘ └┘
src └─┘ └──────────────┘ └─┘
typ ┴ └─┘ └──────────────┘ └┘ └─┘ └┘ └┘
doc └──────────────┘
161 begin
st └─────
162 apply stationary_point_spec hf,
id └───────────────────┘ └┘
src └────┘└───────────────────┘┴
typ └────┘└───────────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────┘└─
163 { apply le_max_left },
id └─────────┘
src └────┘└─────────┘┴
typ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└────────────────┘└┘└
164 { apply le_refl }
id └─────┘
src └────┘└─────┘┴
typ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────┘└─
165 end
st ──┘
166
167 /-- An auxiliary lemma for manipulating sequence indices. -/
168 lemma lift_index_left {f : padic_seq p} (hf : ¬ f ≈ 0) (v1 v3 : ℕ) :
id └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘
169 padic_norm p (f (stationary_point hf)) =
id └────────┘ ┴ ┴ └──────────────┘ └┘ ┴
src └────────┘ └──────────────┘ ┴
typ └────────┘ ┴ ┴ └──────────────┘ └┘ ┴
doc └────────┘ └──────────────┘
170 padic_norm p (f (max v1 (max (stationary_point hf) v3))) :=
id └────────┘ ┴ ┴ └─┘ └┘ └─┘ └──────────────┘ └┘ └┘
src └────────┘ └─┘ └─┘ └──────────────┘
typ └────────┘ ┴ ┴ └─┘ └┘ └─┘ └──────────────┘ └┘ └┘
doc └────────┘ └──────────────┘
171 let i := max v1 (max (stationary_point hf) v3) in
id ┴ └─┘ └┘ └─┘ └──────────────┘ └┘ └┘
src └─┘ └─┘ └──────────────┘
typ ┴ └─┘ └┘ └─┘ └──────────────┘ └┘ └┘
doc └──────────────┘
172 begin
st └─────
173 apply stationary_point_spec hf,
id └───────────────────┘ └┘
src └────┘└───────────────────┘┴
typ └────┘└───────────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────┘└─
174 { apply le_trans,
id └──────┘
src └────┘└──────┘
typ └────┘└──────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└────────────┘└─
175 { apply le_max_left _ v3 },
id └─────────┘ └┘
src └────┘└─────────┘└─┘ ┴
typ └────┘└─────────┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────┘└─────────────────────┘└┘└
176 { apply le_max_right } },
id └──────────┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────┘└──┘└
177 { apply le_refl }
id └─────┘
src └────┘└─────┘┴
typ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────┘└─
178 end
st ──┘
179
180 /-- An auxiliary lemma for manipulating sequence indices. -/
181 lemma lift_index_right {f : padic_seq p} (hf : ¬ f ≈ 0) (v1 v2 : ℕ) :
id └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘
182 padic_norm p (f (stationary_point hf)) =
id └────────┘ ┴ ┴ └──────────────┘ └┘ ┴
src └────────┘ └──────────────┘ ┴
typ └────────┘ ┴ ┴ └──────────────┘ └┘ ┴
doc └────────┘ └──────────────┘
183 padic_norm p (f (max v1 (max v2 (stationary_point hf)))) :=
id └────────┘ ┴ ┴ └─┘ └┘ └─┘ └┘ └──────────────┘ └┘
src └────────┘ └─┘ └─┘ └──────────────┘
typ └────────┘ ┴ ┴ └─┘ └┘ └─┘ └┘ └──────────────┘ └┘
doc └────────┘ └──────────────┘
184 let i := max v1 (max v2 (stationary_point hf)) in
id ┴ └─┘ └┘ └─┘ └┘ └──────────────┘ └┘
src └─┘ └─┘ └──────────────┘
typ ┴ └─┘ └┘ └─┘ └┘ └──────────────┘ └┘
doc └──────────────┘
185 begin
st └─────
186 apply stationary_point_spec hf,
id └───────────────────┘ └┘
src └────┘└───────────────────┘┴
typ └────┘└───────────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────┘└─
187 { apply le_trans,
id └──────┘
src └────┘└──────┘
typ └────┘└──────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└────────────┘└─
188 { apply le_max_right v2 },
id └──────────┘ └┘
src └────┘└──────────┘┴ ┴
typ └────┘└──────────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────┘└────────────────────┘└┘└
189 { apply le_max_right } },
id └──────────┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────┘└──┘└
190 { apply le_refl }
id └─────┘
src └────┘└─────┘┴
typ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────┘└─
191 end
st ──┘
192
193 end embedding
194
195 end padic_seq
196
197 section
198 open padic_seq
199
200 private meta def index_simp_core (hh hf hg : expr)
id └──┘
src └──┘
typ └──┘
doc └──┘
201 (at_ : interactive.loc := interactive.loc.ns [none]) : tactic unit :=
id └─────────────┘ └────────────────┘ ┴└──┘┴ └────┘ └──┘
src └─────────────┘ └────────────────┘ ┴└──┘┴ └────┘ └──┘
typ └─────────────┘ └────────────────┘ ┴└──┘┴ └────┘ └──┘
doc └────────────────┘ └──┘
202 do [v1, v2, v3] ← [hh, hf, hg].mmap
id ┴└┘┴ └┘┴ └┘┴ ┴└┘┴ └┘┴ └┘┴└──┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘
typ ┴└┘┴ └┘┴ └┘┴ ┴└┘┴ └┘┴ └┘┴└──┘
203 (λ n, tactic.mk_app ``stationary_point [n] <|> return n),
id ┴ └───────────┘ ┴ ┴┴┴ └─┘ └────┘ ┴
src └───────────┘ ┴ ┴ ┴ └─┘ └────┘
typ ┴ └───────────┘ ┴ ┴┴┴ └─┘ └────┘ ┴
doc └───────────┘
204 e1 ← tactic.mk_app ``lift_index_left_left [hh, v2, v3] <|> return `(true),
id └┘ └───────────┘ ┴ ┴└┘┴ ┴ ┴ └─┘ └────┘ └──┘
src └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘ └──┘
typ └┘ └───────────┘ ┴ ┴└┘┴ ┴ ┴ └─┘ └────┘ └──┘
doc └───────────┘
205 e2 ← tactic.mk_app ``lift_index_left [hf, v1, v3] <|> return `(true),
id └┘ └───────────┘ ┴ ┴└┘┴ ┴ ┴ └─┘ └────┘ └──┘
src └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘ └──┘
typ └┘ └───────────┘ ┴ ┴└┘┴ ┴ ┴ └─┘ └────┘ └──┘
doc └───────────┘
206 e3 ← tactic.mk_app ``lift_index_right [hg, v1, v2] <|> return `(true),
id └┘ └───────────┘ ┴ ┴└┘┴ ┴ ┴ └─┘ └────┘ └──┘
src └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘ └──┘
typ └┘ └───────────┘ ┴ ┴└┘┴ ┴ ┴ └─┘ └────┘ └──┘
doc └───────────┘
207 sl ← [e1, e2, e3].mfoldl (λ s e, simp_lemmas.add s e) simp_lemmas.mk,
id └┘ ┴└┘┴ └┘┴ └┘┴└────┘ ┴ ┴ └─────────────┘ ┴ ┴ └────────────┘
src ┴ ┴ ┴ ┴└────┘ └─────────────┘ └────────────┘
typ └┘ ┴└┘┴ └┘┴ └┘┴└────┘ ┴ ┴ └─────────────┘ ┴ ┴ └────────────┘
208 when at_.include_goal (tactic.simp_target sl),
id └──┘ └─┘└───────────┘ └────────────────┘ └┘
src └──┘ └───────────┘ └────────────────┘
typ └──┘ └─┘└───────────┘ └────────────────┘ └┘
209 hs ← at_.get_locals, hs.mmap' (tactic.simp_hyp sl [])
id └┘ └─┘└─────────┘ └┘└────┘ └─────────────┘ └┘ └┘
src └─────────┘ └────┘ └─────────────┘ └┘
typ └┘ └─┘└─────────┘ └┘└────┘ └─────────────┘ └┘ └┘
210
211 /--
212 This is a special-purpose tactic that lifts padic_norm (f (stationary_point f)) to
213 padic_norm (f (max _ _ _)).
214 -/
215 meta def tactic.interactive.padic_index_simp (l : interactive.parse interactive.types.pexpr_list)
id └───────────────┘ └──────────────────────────┘
src └───────────────┘ └──────────────────────────┘
typ └───────────────┘ └──────────────────────────┘
doc └───────────────┘
216 (at_ : interactive.parse interactive.types.location) : tactic unit :=
id └───────────────┘ └────────────────────────┘ └────┘ └──┘
src └───────────────┘ └────────────────────────┘ └────┘ └──┘
typ └───────────────┘ └────────────────────────┘ └────┘ └──┘
doc └───────────────┘ └──┘
217 do [h, f, g] ← l.mmap tactic.i_to_expr,
id ┴┴┴ ┴┴ ┴┴ ┴└───┘ └──────────────┘
src ┴ ┴ ┴ ┴ └───┘ └──────────────┘
typ ┴┴┴ ┴┴ ┴┴ ┴└───┘ └──────────────┘
218 index_simp_core h f g at_
id └─────────────┘ └─┘
src └─────────────┘
typ └─────────────┘ └─┘
219 end
220
221 namespace padic_seq
222 section embedding
223
224 open cau_seq
225 variables {p : ℕ} [hp : nat.prime p]
id ┴ └───────┘
src ┴ └───────┘
typ ┴ └───────┘
doc └───────┘
226 include hp
227
228 lemma norm_mul (f g : padic_seq p) : (f * g).norm = f.norm * g.norm :=
id └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴└───┘ ┴ ┴└───┘
src └───────┘ ┴ └──┘ ┴ └───┘ ┴ └───┘
typ └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴└───┘ ┴ ┴└───┘
doc └───────┘ └──┘ └───┘ └───┘
229 if hf : f ≈ 0 then
id └┘ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴
230 have hg : f * g ≈ 0, from mul_equiv_zero' _ hf,
id ┴ ┴ ┴ ┴ └─────────────┘ └┘
src ┴ ┴ └─────────────┘
typ ┴ ┴ ┴ ┴ └─────────────┘ └┘
231 by simp [hf, hg, norm]
id └┘ └┘ └──┘
src └────┘ └┘ └┘└──┘└┘
typ └────┘└┘└┘└┘└┘└──┘└┘
doc └────┘ └┘ └┘└──┘└┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st └───────────────────┘
232 else if hg : g ≈ 0 then
id └┘ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴
233 have hf : f * g ≈ 0, from mul_equiv_zero _ hg,
id ┴ ┴ ┴ ┴ └────────────┘ └┘
src ┴ ┴ └────────────┘
typ ┴ ┴ ┴ ┴ └────────────┘ └┘
234 by simp [hf, hg, norm]
id └┘ └┘ └──┘
src └────┘ └┘ └┘└──┘└┘
typ └────┘└┘└┘└┘└┘└──┘└┘
doc └────┘ └┘ └┘└──┘└┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st └───────────────────┘
235 else
236 have hfg : ¬ f * g ≈ 0, by apply mul_not_equiv_zero; assumption,
id └──┘ ┴ ┴ ┴ ┴ ┴ └────────────────┘
src ┴ ┴ ┴ └────┘└────────────────┘ └────────┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘└────────────────┘ └────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴
st └───────────────────────────────────┘
237 begin
st └─────
238 unfold norm,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
239 split_ifs,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ────────────┘└─
240 padic_index_simp [hfg, hf, hg],
id └─┘ └┘ └┘
src └────────────────┘ └┘ └┘ ┴
typ └────────────────┘└─┘└┘└┘└┘└┘┴
doc └────────────────┘ └┘ └┘ ┴
txt └────────────────┘ └┘ └┘ ┴
par └────────────────┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ─────────────────────────────────┘└─
241 apply padic_norm.mul
id └────────────┘
src └────┘└────────────┘└
typ └────┘└────────────┘└
doc └────┘└────────────┘└
txt └────┘ └
par └────┘ └
pid ┴ └
st ─────────────────────────
242 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
243
244 lemma eq_zero_iff_equiv_zero (f : padic_seq p) : mk f = 0 ↔ f ≈ 0 :=
id └───────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ └┘ ┴ ┴ ┴
typ └───────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘
245 mk_eq
id └───┘
src └───┘
typ └───┘
246
247 lemma ne_zero_iff_nequiv_zero (f : padic_seq p) : mk f ≠ 0 ↔ ¬ f ≈ 0 :=
id └───────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ └┘ ┴ ┴ ┴ ┴
typ └───────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
248 not_iff_not.2 (eq_zero_iff_equiv_zero _)
id └─────────┘┴ └────────────────────┘
src └─────────┘┴ └────────────────────┘
typ └─────────┘┴ └────────────────────┘
249
250 lemma norm_const (q : ℚ) : norm (const (padic_norm p) q) = padic_norm p q :=
id ┴ └──┘ └───┘ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴
src ┴ └──┘ └───┘ └────────┘ ┴ └────────┘
typ ┴ └──┘ └───┘ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴
doc ┴ └──┘ └───┘ └────────┘ └────────┘
251 if hq : q = 0 then
id └┘ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴
252 have (const (padic_norm p) q) ≈ 0,
id └───┘ └────────┘ ┴ ┴ ┴
src └───┘ └────────┘ ┴
typ └───┘ └────────┘ ┴ ┴ ┴
doc └───┘ └────────┘
253 by simp [hq]; apply setoid.refl (const (padic_norm p) 0),
id └┘ └─────────┘ └───┘ └────────┘ ┴
src └────┘ ┴ └────┘└─────────┘┴ └───┘┴ └────────┘┴ └──┘
typ └────┘└┘┴ └────┘└─────────┘┴ └───┘┴ └────────┘┴┴└──┘
doc └────┘ ┴ └────┘ ┴ └───┘┴ └────────┘┴ └──┘
txt └────┘ ┴ └────┘ ┴ ┴ ┴ └──┘
par └────┘ ┴ └────┘ ┴ ┴ ┴ └──┘
pid ┴┴ ┴ ┴ ┴ ┴ ┴ └──┘
st └────────────────────────────────────────────────────┘
254 by subst hq; simp [norm, this]
id └┘ └──┘ └──┘
src └────┘ └────┘└──┘└┘ └┘
typ └────┘└┘ └────┘└──┘└┘└──┘└┘
doc └────┘ └────┘└──┘└┘ └┘
txt └────┘ └────┘ └┘ └┘
par └────┘ └────┘ └┘ └┘
pid ┴ ┴┴ └┘ ┴┴
st └───────────────────────────┘
255 else
256 have ¬ (const (padic_norm p) q) ≈ 0, from not_equiv_zero_const_of_nonzero hq,
id └──┘ ┴ └───┘ └────────┘ ┴ ┴ ┴ └─────────────────────────────┘ └┘
src ┴ └───┘ └────────┘ ┴ └─────────────────────────────┘
typ └──┘ ┴ └───┘ └────────┘ ┴ ┴ ┴ └─────────────────────────────┘ └┘
doc └───┘ └────────┘
257 by simp [norm, this]
id └──┘ └──┘
src └────┘└──┘└┘ └─
typ └────┘└──┘└┘└──┘└─
doc └────┘└──┘└┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────────
258
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
259 lemma norm_image (a : padic_seq p) (ha : ¬ a ≈ 0) :
id └───────┘ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
260 (∃ (n : ℤ), a.norm = ↑p ^ (-n)) :=
id ┴ ┴ ┴ ┴└───┘ ┴ ┴┴ ┴ ┴┴
src ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴└───┘ ┴ ┴┴ ┴ ┴┴
doc └───┘
261 let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha in
id └─┘ └─────────────────────────┘ └┘
src └─────────────────────────┘
typ └─┘ └─────────────────────────┘ └┘
262 by simpa [hk] using padic_norm.image p hk'
id └┘ └──────────────┘ ┴ └─┘
src └─────┘ └──────┘└──────────────┘┴ ┴ └
typ └─────┘└┘└──────┘└──────────────┘┴┴┴└─┘└
doc └─────┘ └──────┘└──────────────┘┴ ┴ └
txt └─────┘ └──────┘ ┴ ┴ └
par └─────┘ └──────┘ ┴ ┴ └
pid ┴┴ ┴┴└────┘ ┴ ┴ └
st └────────────────────────────────────────
263
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
264 lemma norm_one : norm (1 : padic_seq p) = 1 :=
id └──┘ └───────┘ ┴ ┴
src └──┘ └───────┘ ┴
typ └──┘ └───────┘ ┴ ┴
doc └──┘ └───────┘
265 have h1 : ¬ (1 : padic_seq p) ≈ 0, from one_not_equiv_zero _,
id ┴ └───────┘ ┴ ┴ └────────────────┘
src ┴ └───────┘ ┴ └────────────────┘
typ ┴ └───────┘ ┴ ┴ └────────────────┘
doc └───────┘
266 by simp [h1, norm, hp.one_lt]
id └┘ └──┘
src └────┘ └┘└──┘└┘ └─
typ └────┘└┘└┘└──┘└┘└───────┘└─
doc └────┘ └┘└──┘└┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └───────────────────────────
267
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
268 private lemma norm_eq_of_equiv_aux {f g : padic_seq p} (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0) (hfg : f ≈ g)
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
269 (h : padic_norm p (f (stationary_point hf)) ≠ padic_norm p (g (stationary_point hg)))
id └────────┘ ┴ ┴ └──────────────┘ └┘ ┴ └────────┘ ┴ ┴ └──────────────┘ └┘
src └────────┘ └──────────────┘ ┴ └────────┘ └──────────────┘
typ └────────┘ ┴ ┴ └──────────────┘ └┘ ┴ └────────┘ ┴ ┴ └──────────────┘ └┘
doc └────────┘ └──────────────┘ └────────┘ └──────────────┘
270 (hgt : padic_norm p (f (stationary_point hf)) > padic_norm p (g (stationary_point hg))) :
id └────────┘ ┴ ┴ └──────────────┘ └┘ ┴ └────────┘ ┴ ┴ └──────────────┘ └┘
src └────────┘ └──────────────┘ ┴ └────────┘ └──────────────┘
typ └────────┘ ┴ ┴ └──────────────┘ └┘ ┴ └────────┘ ┴ ┴ └──────────────┘ └┘
doc └────────┘ └──────────────┘ └────────┘ └──────────────┘
271 false :=
id └───┘
src └───┘
typ └───┘
272 begin
st └─────
273 have hpn : padic_norm p (f (stationary_point hf)) - padic_norm p (g (stationary_point hg)) > 0,
id ┴ └┘ ┴ └────────┘ ┴ ┴ └──────────────┘ └┘ ┴
src └─────────┘ ┴ ┴ ┴ ┴ └─┘┴┴└────────┘┴ ┴ ┴ └──────────────┘┴ └─┘┴└┘
typ └─────────┘ ┴ ┴ ┴┴ ┴└┘└─┘┴┴└────────┘┴┴┴ ┴┴ └──────────────┘┴└┘└─┘┴└┘
doc └─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴└────────┘┴ ┴ ┴ └──────────────┘┴ └─┘ └┘
txt └─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
par └─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
pid └──────┘└─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴┴
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
274 from sub_pos_of_lt hgt,
id └───────────┘ └─┘
src └───┘└───────────┘┴
typ └───┘└───────────┘┴└─┘
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └───┘ ┴
st ─────────────────────────┘└─
275 cases hfg _ hpn with N hN,
id └─┘ └─┘
src └────┘ └─┘ └────────┘
typ └────┘└─┘└─┘└─┘└────────┘
doc └────┘ └─┘ └────────┘
txt └────┘ └─┘ └────────┘
par └────┘ └─┘ └────────┘
pid ┴ └─┘ └────────┘
st ──────────────────────────┘└─
276 let i := max N (max (stationary_point hf) (stationary_point hg)),
id ┴ └─┘ └┘ └──────────────┘ └┘
src └───────┘ ┴ ┴ └─┘┴ ┴ └┘ └──────────────┘┴ └┘
typ └───────┘ ┴┴┴ └─┘┴ ┴└┘└┘ └──────────────┘┴└┘└┘
doc └───────┘ ┴ ┴ ┴ ┴ └┘ └──────────────┘┴ └┘
txt └───────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘
par └───────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘
pid └───┘┴└─┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘
st ─────────────────────────────────────────────────────────────────┘└─
277 have hi : i ≥ N, from le_max_left _ _,
id ┴ ┴ ┴ └─────────┘
src └────────┘ ┴┴┴ └───┘└─────────┘└──┘
typ └────────┘┴┴┴┴┴ └───┘└─────────┘└──┘
doc └────────┘ ┴ ┴ └───┘ └──┘
txt └────────┘ ┴ ┴ └───┘ └──┘
par └────────┘ ┴ ┴ └───┘ └──┘
pid └─────┘└─┘ ┴ ┴ └───┘ └──┘
st ────────────────┘└────────────────────┘└─
278 have hN' := hN _ hi,
id └┘ └┘
src └──────────┘ └─┘
typ └──────────┘└┘└─┘└┘
doc └──────────┘ └─┘
txt └──────────┘ └─┘
par └──────────┘ └─┘
pid └──────┘┴└─┘ └─┘
st ────────────────────┘└─
279 padic_index_simp [N, hf, hg] at hN' h hgt,
id ┴ └┘ └┘
src └────────────────┘ └┘ └┘ └────────────┘
typ └────────────────┘┴└┘└┘└┘└┘└────────────┘
doc └────────────────┘ └┘ └┘ └────────────┘
txt └────────────────┘ └┘ └┘ └────────────┘
par └────────────────┘ └┘ └┘ └────────────┘
pid └┘ └┘ └┘ ┴└───────────┘
st ──────────────────────────────────────────┘└─
280 have hpne : padic_norm p (f i) ≠ padic_norm p (-(g i)),
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴ └┘┴┴└────────┘┴ ┴ ┴ ┴ └┘
typ └──────────┘ ┴ ┴ ┴┴ └┘┴┴└────────┘┴┴┴ ┴ ┴┴┴└┘
doc └──────────┘ ┴ ┴ ┴ └┘ ┴└────────┘┴ ┴ ┴ └┘
txt └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid └───────┘└─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────────┘
281 by rwa [ ←padic_norm.neg p (g i)] at h,
id └────────────┘ ┴ ┴ ┴
src └─────┘└────────────┘┴ ┴ ┴ └─────┘
typ └─────┘└────────────┘┴┴┴ ┴┴┴└─────┘
doc └─────┘└────────────┘┴ ┴ ┴ └─────┘
txt └─────┘ ┴ ┴ ┴ └─────┘
par └─────┘ ┴ ┴ ┴ └─────┘
pid └──┘ ┴ ┴ ┴ └┘└───┘
st └──────────────────────┘┴ └─
282 let hpnem := add_eq_max_of_ne p hpne,
id └──────────────┘ ┴ └──┘
src └───────────┘└──────────────┘┴ ┴
typ └───────────┘└──────────────┘┴┴┴└──┘
doc └───────────┘└──────────────┘┴ ┴
txt └───────────┘ ┴ ┴
par └───────────┘ ┴ ┴
pid └───────┘┴└─┘ ┴ ┴
st ─────────────────────────────────────┘└─
283 have hpeq : padic_norm p ((f - g) i) = max (padic_norm p (f i)) (padic_norm p (g i)),
id ┴ └─┘ ┴ └────────┘ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴ ┴ └┘ └┘┴┴└─┘┴ ┴ ┴ ┴ └─┘ └────────┘┴ ┴ ┴ └┘
typ └──────────┘ ┴ ┴ ┴ ┴ └┘ └┘┴┴└─┘┴ ┴ ┴ ┴┴ └─┘ └────────┘┴┴┴ ┴┴┴└┘
doc └──────────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────────┘┴ ┴ ┴ └┘
txt └──────────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘
par └──────────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘
pid └───────┘└─┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────────────────────┘└─
284 { rwa padic_norm.neg at hpnem },
id └────────────┘
src └──┘└────────────┘└────────┘
typ └──┘└────────────┘└────────┘
doc └──┘└────────────┘└────────┘
txt └──┘ └────────┘
par └──┘ └────────┘
pid ┴ └───────┘┴
st ───┘└──────────────────────────┘└┘└
285 rw [hpeq, max_eq_left_of_lt hgt] at hN',
id └──┘ └───────────────┘ └─┘
src └──┘ └┘└───────────────┘┴ └──────┘
typ └──┘└──┘└┘└───────────────┘┴└─┘└──────┘
doc └──┘ └┘ ┴ └──────┘
txt └──┘ └┘ ┴ └──────┘
par └──┘ └┘ ┴ └──────┘
pid └┘ └┘ ┴ ┴└─────┘
st ─────────┘└─────────────────────┘┴└─────┘└─
286 have : padic_norm p (f i) < padic_norm p (f i),
id ┴ └────────┘ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ └┘┴┴└────────┘┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ └┘┴┴└────────┘┴┴┴ ┴┴┴┴
doc └─────┘ ┴ ┴ ┴ └┘ ┴└────────┘┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────┘└─
287 { apply lt_of_lt_of_le hN', apply sub_le_self, apply padic_norm.nonneg },
id └────────────┘ └─┘ └─────────┘ └───────────────┘
src └────┘└────────────┘┴ └────┘└─────────┘ └────┘└───────────────┘┴
typ └────┘└────────────┘┴└─┘ └────┘└─────────┘ └────┘└───────────────┘┴
doc └────┘ ┴ └────┘ └────┘└───────────────┘┴
txt └────┘ ┴ └────┘ └────┘ ┴
par └────┘ ┴ └────┘ └────┘ ┴
pid ┴ ┴ ┴ ┴ ┴
st ───┘└──────────────────────┘└─────────────────┘└────────────────────────┘└┘└
288 exact lt_irrefl _ this
id └───────┘ └──┘
src └────┘└───────┘└─┘ ┴
typ └────┘└───────┘└─┘└──┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ────────────────────────┘
289 end
st └─┘
290
291 private lemma norm_eq_of_equiv {f g : padic_seq p} (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0) (hfg : f ≈ g) :
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
292 padic_norm p (f (stationary_point hf)) = padic_norm p (g (stationary_point hg)) :=
id └────────┘ ┴ ┴ └──────────────┘ └┘ ┴ └────────┘ ┴ ┴ └──────────────┘ └┘
src └────────┘ └──────────────┘ ┴ └────────┘ └──────────────┘
typ └────────┘ ┴ ┴ └──────────────┘ └┘ ┴ └────────┘ ┴ ┴ └──────────────┘ └┘
doc └────────┘ └──────────────┘ └────────┘ └──────────────┘
293 begin
st └─────
294 by_contradiction h,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └┘
st ───────────────────┘└─
295 cases (decidable.em (padic_norm p (f (stationary_point hf)) >
id └──────────┘ ┴ └┘ ┴
src └────┘ └──────────┘┴ ┴ ┴ ┴ ┴ └─┘┴└
typ └────┘ └──────────┘┴ ┴ ┴ ┴┴ ┴└┘└─┘┴└
doc └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └
txt └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └
par └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ────────────────────────────────────────────────────────────────
296 padic_norm p (g (stationary_point hg))))
id └────────┘ ┴ ┴ └──────────────┘ └┘
src ─────────┘└────────┘┴ ┴ ┴ └──────────────┘┴ └────
typ ─────────┘└────────┘┴┴┴ ┴┴ └──────────────┘┴└┘└────
doc ─────────┘└────────┘┴ ┴ ┴ └──────────────┘┴ └────
txt ─────────┘ ┴ ┴ ┴ ┴ └────
par ─────────┘ ┴ ┴ ┴ ┴ └────
pid ─────────┘ ┴ ┴ ┴ ┴ └──┘└
st ───────────────────────────────────────────────────
297 with hgt hngt,
src ──────────────────┘
typ ──────────────────┘
doc ──────────────────┘
txt ──────────────────┘
par ──────────────────┘
pid ──────────────────┘
st ──────────────────┘└─
298 { exact norm_eq_of_equiv_aux hf hg hfg h hgt },
id └──────────────────┘ └┘ └┘ └─┘ ┴ └─┘
src └────┘└──────────────────┘┴ ┴ ┴ ┴ ┴ ┴
typ └────┘└──────────────────┘┴└┘┴└┘┴└─┘┴┴┴└─┘┴
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───┘└─────────────────────────────────────────┘└┘└
299 { apply norm_eq_of_equiv_aux hg hf (setoid.symm hfg) (ne.symm h),
id └──────────────────┘ └┘ └┘ └─────────┘ └─┘ └─────┘ ┴
src └────┘└──────────────────┘┴ ┴ ┴ └─────────┘┴ └┘ └─────┘┴ ┴
typ └────┘└──────────────────┘┴└┘┴└┘┴ └─────────┘┴└─┘└┘ └─────┘┴┴┴
doc └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ─────────────────────────────────────────────────────────────────┘└─
300 apply lt_of_le_of_ne,
id └────────────┘
src └────┘└────────────┘
typ └────┘└────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────┘└─
301 apply le_of_not_gt hngt,
id └──────────┘ └──┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴└──┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────┘└─
302 apply h }
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────┘└─
303 end
st ──┘
304
305 theorem norm_equiv {f g : padic_seq p} (hfg : f ≈ g) : f.norm = g.norm :=
id └───────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴└───┘
src └───────┘ ┴ └───┘ ┴ └───┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴└───┘
doc └───────┘ └───┘ └───┘
306 if hf : f ≈ 0 then
id └┘ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴
307 have hg : g ≈ 0, from setoid.trans (setoid.symm hfg) hf,
id ┴ ┴ └──────────┘ └─────────┘ └─┘ └┘
src ┴ └──────────┘ └─────────┘
typ ┴ ┴ └──────────┘ └─────────┘ └─┘ └┘
308 by simp [norm, hf, hg]
id └──┘ └┘ └┘
src └────┘└──┘└┘ └┘ └┘
typ └────┘└──┘└┘└┘└┘└┘└┘
doc └────┘└──┘└┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st └───────────────────┘
309 else have hg : ¬ g ≈ 0, from hf ∘ setoid.trans hfg,
id └──┘ ┴ ┴ ┴ └┘ ┴ └──────────┘ └─┘
src ┴ ┴ ┴ └──────────┘
typ └──┘ ┴ ┴ ┴ └┘ ┴ └──────────┘ └─┘
310 by unfold norm; split_ifs; exact norm_eq_of_equiv hf hg hfg
id └──────────────┘ └┘ └┘ └─┘
src └─────────┘ └───────┘ └────┘└──────────────┘┴ ┴ ┴ └
typ └─────────┘ └───────┘ └────┘└──────────────┘┴└┘┴└┘┴└─┘└
doc └─────────┘ └───────┘ └────┘ ┴ ┴ ┴ └
txt └─────────┘ └───────┘ └────┘ ┴ ┴ ┴ └
par └─────────┘ └───────┘ └────┘ ┴ ┴ ┴ └
pid └───┘ ┴ ┴ ┴ ┴ └
st └─────────────────────────────────────────────────────────
311
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
312 private lemma norm_nonarchimedean_aux {f g : padic_seq p}
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
doc └───────┘
313 (hfg : ¬ f + g ≈ 0) (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0) : (f + g).norm ≤ max (f.norm) (g.norm) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴└───┘ ┴└───┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ └───┘ └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴└───┘ ┴└───┘
doc └──┘ └───┘ └───┘
314 begin
st └─────
315 unfold norm, split_ifs,
src └─────────┘ └───────┘
typ └─────────┘ └───────┘
doc └─────────┘ └───────┘
txt └─────────┘ └───────┘
par └─────────┘ └───────┘
pid └───┘
st ────────────┘└─────────┘└─
316 padic_index_simp [hfg, hf, hg],
id └─┘ └┘ └┘
src └────────────────┘ └┘ └┘ ┴
typ └────────────────┘└─┘└┘└┘└┘└┘┴
doc └────────────────┘ └┘ └┘ ┴
txt └────────────────┘ └┘ └┘ ┴
par └────────────────┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ───────────────────────────────┘└─
317 apply padic_norm.nonarchimedean
id └───────────────────────┘
src └────┘└───────────────────────┘┴
typ └────┘└───────────────────────┘┴
doc └────┘└───────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────────┘
318 end
st └─┘
319
320 theorem norm_nonarchimedean (f g : padic_seq p) : (f + g).norm ≤ max (f.norm) (g.norm) :=
id └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴└───┘ ┴└───┘
src └───────┘ ┴ └──┘ ┴ └─┘ └───┘ └───┘
typ └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴└───┘ ┴└───┘
doc └───────┘ └──┘ └───┘ └───┘
321 if hfg : f + g ≈ 0 then
id └┘ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴
322 have 0 ≤ max (f.norm) (g.norm), from le_max_left_of_le (norm_nonneg _),
id ┴ └─┘ ┴└───┘ ┴└───┘ └───────────────┘ └─────────┘
src ┴ └─┘ └───┘ └───┘ └───────────────┘ └─────────┘
typ ┴ └─┘ ┴└───┘ ┴└───┘ └───────────────┘ └─────────┘
doc └───┘ └───┘
323 by simpa [hfg, norm]
id └─┘ └──┘
src └─────┘ └┘└──┘└┘
typ └─────┘└─┘└┘└──┘└┘
doc └─────┘ └┘└──┘└┘
txt └─────┘ └┘ └┘
par └─────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st └─────────────────┘
324 else if hf : f ≈ 0 then
id └┘ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴
325 have hfg' : f + g ≈ g,
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
326 { change lim_zero (f - 0) at hf,
id └──────┘ ┴ ┴
src └─────┘└──────┘┴ ┴┴└───────┘
typ └─────┘└──────┘┴ ┴┴┴└───────┘
doc └─────┘└──────┘┴ ┴ └───────┘
txt └─────┘ ┴ ┴ └───────┘
par └─────┘ ┴ ┴ └───────┘
pid ┴ ┴ ┴ └─┘┴└───┘
st └─────────────────────────────┘└─
327 show lim_zero (f + g - g), by simpa using hf },
id └──────┘ ┴ ┴ ┴ └┘
src └───┘└──────┘┴ ┴┴┴ ┴ ┴ ┴ └──────────┘ ┴
typ └───┘└──────┘┴ ┴┴┴┴ ┴ ┴┴┴ └──────────┘└┘┴
doc └───┘└──────┘┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
txt └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
par └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
pid └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────┘ ┴
st ────────────────────────────┘ └┘
328 have hcfg : (f + g).norm = g.norm, from norm_equiv hfg',
id ┴ ┴ ┴ └──┘ ┴ ┴└───┘ └────────┘ └──┘
src ┴ └──┘ ┴ └───┘ └────────┘
typ ┴ ┴ ┴ └──┘ ┴ ┴└───┘ └────────┘ └──┘
doc └──┘ └───┘
329 have hcl : f.norm = 0, from (norm_zero_iff f).2 hf,
id ┴└───┘ ┴ └───────────┘ ┴ ┴ └┘
src └───┘ ┴ └───────────┘ ┴
typ ┴└───┘ ┴ └───────────┘ ┴ ┴ └┘
doc └───┘
330 have max (f.norm) (g.norm) = g.norm,
id └─┘ ┴└───┘ ┴└───┘ ┴ ┴└───┘
src └─┘ └───┘ └───┘ ┴ └───┘
typ └─┘ ┴└───┘ ┴└───┘ ┴ ┴└───┘
doc └───┘ └───┘ └───┘
331 by rw hcl; exact max_eq_right (norm_nonneg _),
id └─┘ └──────────┘ └─────────┘
src └─┘ └────┘└──────────┘┴ └─────────┘└─┘
typ └─┘└─┘ └────┘└──────────┘┴ └─────────┘└─┘
doc └─┘ └────┘ ┴ └─┘
txt └─┘ └────┘ ┴ └─┘
par └─┘ └────┘ ┴ └─┘
pid ┴ ┴ ┴ └─┘
st └─────────────────────────────────────────┘
332 by rw [this, hcfg]
id └──┘ └──┘
src └──┘ └┘ └┘
typ └──┘└──┘└┘└──┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └───────┘└────┘┴┴
333 else if hg : g ≈ 0 then
id └┘ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴
334 have hfg' : f + g ≈ f,
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
335 { change lim_zero (g - 0) at hg,
id └──────┘ ┴
src └─────┘└──────┘┴ ┴ └───────┘
typ └─────┘└──────┘┴ ┴┴ └───────┘
doc └─────┘└──────┘┴ ┴ └───────┘
txt └─────┘ ┴ ┴ └───────┘
par └─────┘ ┴ ┴ └───────┘
pid ┴ ┴ ┴ └─┘┴└───┘
st └─────────────────────────────┘└─
336 show lim_zero (f + g - f), by simpa [add_sub_cancel'] using hg },
id └──────┘ ┴ ┴ └─────────────┘ └┘
src └───┘└──────┘┴ ┴ ┴ ┴ ┴ ┴ └─────┘└─────────────┘└──────┘ ┴
typ └───┘└──────┘┴ ┴ ┴┴┴ ┴┴┴ └─────┘└─────────────┘└──────┘└┘┴
doc └───┘└──────┘┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └──────┘ ┴
txt └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └──────┘ ┴
par └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └──────┘ ┴
pid └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴└────┘ ┴
st ────────────────────────────┘ └┘
337 have hcfg : (f + g).norm = f.norm, from norm_equiv hfg',
id ┴ ┴ ┴ └──┘ ┴ ┴└───┘ └────────┘ └──┘
src ┴ └──┘ ┴ └───┘ └────────┘
typ ┴ ┴ ┴ └──┘ ┴ ┴└───┘ └────────┘ └──┘
doc └──┘ └───┘
338 have hcl : g.norm = 0, from (norm_zero_iff g).2 hg,
id ┴└───┘ ┴ └───────────┘ ┴ ┴ └┘
src └───┘ ┴ └───────────┘ ┴
typ ┴└───┘ ┴ └───────────┘ ┴ ┴ └┘
doc └───┘
339 have max (f.norm) (g.norm) = f.norm,
id └─┘ ┴└───┘ ┴└───┘ ┴ ┴└───┘
src └─┘ └───┘ └───┘ ┴ └───┘
typ └─┘ ┴└───┘ ┴└───┘ ┴ ┴└───┘
doc └───┘ └───┘ └───┘
340 by rw hcl; exact max_eq_left (norm_nonneg _),
id └─┘ └─────────┘ └─────────┘
src └─┘ └────┘└─────────┘┴ └─────────┘└─┘
typ └─┘└─┘ └────┘└─────────┘┴ └─────────┘└─┘
doc └─┘ └────┘ ┴ └─┘
txt └─┘ └────┘ ┴ └─┘
par └─┘ └────┘ ┴ └─┘
pid ┴ ┴ ┴ └─┘
st └────────────────────────────────────────┘
341 by rw [this, hcfg]
id └──┘ └──┘
src └──┘ └┘ └┘
typ └──┘└──┘└┘└──┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └───────┘└────┘┴┴
342 else norm_nonarchimedean_aux hfg hf hg
id └─────────────────────┘ └─┘ └┘ └┘
src └─────────────────────┘
typ └─────────────────────┘ └─┘ └┘ └┘
343
344 lemma norm_eq {f g : padic_seq p} (h : ∀ k, padic_norm p (f k) = padic_norm p (g k)) :
id └───────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
src └───────┘ └────────┘ ┴ └────────┘
typ └───────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └───────┘ └────────┘ └────────┘
345 f.norm = g.norm :=
id ┴└───┘ ┴ ┴└───┘
src └───┘ ┴ └───┘
typ ┴└───┘ ┴ ┴└───┘
doc └───┘ └───┘
346 if hf : f ≈ 0 then
id └┘ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴
347 have hg : g ≈ 0, from equiv_zero_of_val_eq_of_equiv_zero h hf,
id ┴ ┴ └────────────────────────────────┘ ┴ └┘
src ┴ └────────────────────────────────┘
typ ┴ ┴ └────────────────────────────────┘ ┴ └┘
348 by simp [hf, hg, norm]
id └┘ └┘ └──┘
src └────┘ └┘ └┘└──┘└┘
typ └────┘└┘└┘└┘└┘└──┘└┘
doc └────┘ └┘ └┘└──┘└┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st └───────────────────┘
349 else
350 have hg : ¬ g ≈ 0, from λ hg, hf $ equiv_zero_of_val_eq_of_equiv_zero (by simp [h]) hg,
id └──┘ ┴ ┴ ┴ └┘ └┘ └────────────────────────────────┘ ┴ └┘
src ┴ ┴ └────────────────────────────────┘ └────┘ ┴
typ └──┘ ┴ ┴ ┴ └┘ └┘ └────────────────────────────────┘ └────┘┴┴ └┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────┘
351 begin
st └─────
352 simp [hg, hf, norm],
id └┘ └┘ └──┘
src └────┘ └┘ └┘└──┘┴
typ └────┘└┘└┘└┘└┘└──┘┴
doc └────┘ └┘ └┘└──┘┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st ──────────────────────┘└─
353 let i := max (stationary_point hf) (stationary_point hg),
id └─┘ └┘ └──────────────┘ └┘
src └───────┘└─┘┴ ┴ └┘ └──────────────┘┴ ┴
typ └───────┘└─┘┴ ┴└┘└┘ └──────────────┘┴└┘┴
doc └───────┘ ┴ ┴ └┘ └──────────────┘┴ ┴
txt └───────┘ ┴ ┴ └┘ ┴ ┴
par └───────┘ ┴ ┴ └┘ ┴ ┴
pid └───┘┴└─┘ ┴ ┴ └┘ ┴ ┴
st ───────────────────────────────────────────────────────────┘└─
354 have hpf : padic_norm p (f (stationary_point hf)) = padic_norm p (f i),
id └──────────────┘ └┘ ┴ └────────┘ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴ └──────────────┘┴ └─┘┴┴└────────┘┴ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ └──────────────┘┴└┘└─┘┴┴└────────┘┴┴┴ ┴┴┴┴
doc └─────────┘ ┴ ┴ ┴ └──────────────┘┴ └─┘ ┴└────────┘┴ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
pid └──────┘└─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────┘└─
355 { apply stationary_point_spec, apply le_max_left, apply le_refl },
id └───────────────────┘ └─────────┘ └─────┘
src └────┘└───────────────────┘ └────┘└─────────┘ └────┘└─────┘┴
typ └────┘└───────────────────┘ └────┘└─────────┘ └────┘└─────┘┴
doc └────┘ └────┘ └────┘ ┴
txt └────┘ └────┘ └────┘ ┴
par └────┘ └────┘ └────┘ ┴
pid ┴ ┴ ┴ ┴
st ─────┘└─────────────────────────┘└─────────────────┘└──────────────┘└┘└
356 have hpg : padic_norm p (g (stationary_point hg)) = padic_norm p (g i),
id └──────────────┘ └┘ └────────┘ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴ └──────────────┘┴ └─┘ ┴└────────┘┴ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ └──────────────┘┴└┘└─┘ ┴└────────┘┴┴┴ ┴┴┴┴
doc └─────────┘ ┴ ┴ ┴ └──────────────┘┴ └─┘ ┴└────────┘┴ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
pid └──────┘└─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────┘└─
357 { apply stationary_point_spec, apply le_max_right, apply le_refl },
id └───────────────────┘ └──────────┘ └─────┘
src └────┘└───────────────────┘ └────┘└──────────┘ └────┘└─────┘┴
typ └────┘└───────────────────┘ └────┘└──────────┘ └────┘└─────┘┴
doc └────┘ └────┘ └────┘ ┴
txt └────┘ └────┘ └────┘ ┴
par └────┘ └────┘ └────┘ ┴
pid ┴ ┴ ┴ ┴
st ─────┘└─────────────────────────┘└──────────────────┘└──────────────┘└┘└
358 rw [hpf, hpg, h]
id └─┘ └─┘ ┴
src └──┘ └┘ └┘ └─
typ └──┘└─┘└┘└─┘└┘┴└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st ──────────┘└───┘└─┘┴└
359 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
360
361 lemma norm_neg (a : padic_seq p) : (-a).norm = a.norm :=
id └───────┘ ┴ ┴┴ └──┘ ┴ ┴└───┘
src └───────┘ ┴ └──┘ ┴ └───┘
typ └───────┘ ┴ ┴┴ └──┘ ┴ ┴└───┘
doc └───────┘ └──┘ └───┘
362 norm_eq $ by simp
id └─────┘
src └─────┘ └────
typ └─────┘ └────
doc └────
txt └────
par └────
pid └
st └─────
363
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
364 lemma norm_eq_of_add_equiv_zero {f g : padic_seq p} (h : f + g ≈ 0) : f.norm = g.norm :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴└───┘
src └───────┘ ┴ ┴ └───┘ ┴ └───┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴└───┘
doc └───────┘ └───┘ └───┘
365 have lim_zero (f + g - 0), from h,
id └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘
366 have f ≈ -g, from show lim_zero (f - (-g)), by simpa,
id ┴ ┴ ┴┴ └──────┘ ┴ ┴ ┴┴
src ┴ ┴ └──────┘ ┴ ┴ └───┘
typ ┴ ┴ ┴┴ └──────┘ ┴ ┴ ┴┴ └───┘
doc └──────┘ └───┘
txt └───┘
par └───┘
st └────┘
367 have f.norm = (-g).norm, from norm_equiv this,
id ┴└───┘ ┴ ┴┴ └──┘ └────────┘ └──┘
src └───┘ ┴ ┴ └──┘ └────────┘
typ ┴└───┘ ┴ ┴┴ └──┘ └────────┘ └──┘
doc └───┘ └──┘
368 by simpa [norm_neg] using this
id └──────┘ └──┘
src └─────┘└──────┘└──────┘ └
typ └─────┘└──────┘└──────┘└──┘└
doc └─────┘ └──────┘ └
txt └─────┘ └──────┘ └
par └─────┘ └──────┘ └
pid ┴┴ ┴┴└────┘ └
st └────────────────────────────
369
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
370 lemma add_eq_max_of_ne {f g : padic_seq p} (hfgne : f.norm ≠ g.norm) :
id └───────┘ ┴ ┴└───┘ ┴ ┴└───┘
src └───────┘ └───┘ ┴ └───┘
typ └───────┘ ┴ ┴└───┘ ┴ ┴└───┘
doc └───────┘ └───┘ └───┘
371 (f + g).norm = max f.norm g.norm :=
id ┴ ┴ ┴ └──┘ ┴ └─┘ ┴└───┘ ┴└───┘
src ┴ └──┘ ┴ └─┘ └───┘ └───┘
typ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴└───┘ ┴└───┘
doc └──┘ └───┘ └───┘
372 have hfg : ¬f + g ≈ 0, from mt norm_eq_of_add_equiv_zero hfgne,
id ┴┴ ┴ ┴ ┴ └┘ └───────────────────────┘ └───┘
src ┴ ┴ ┴ └┘ └───────────────────────┘
typ ┴┴ ┴ ┴ ┴ └┘ └───────────────────────┘ └───┘
373 if hf : f ≈ 0 then
id └┘ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴
374 have lim_zero (f - 0), from hf,
id └──────┘ ┴ ┴ └┘
src └──────┘ ┴
typ └──────┘ ┴ ┴ └┘
doc └──────┘
375 have f + g ≈ g, from show lim_zero ((f + g) - g), by simpa,
id ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──────┘ ┴ ┴ └───┘
typ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └───┘
doc └──────┘ └───┘
txt └───┘
par └───┘
st └────┘
376 have h1 : (f+g).norm = g.norm, from norm_equiv this,
id ┴┴┴ └──┘ ┴ ┴└───┘ └────────┘ └──┘
src ┴ └──┘ ┴ └───┘ └────────┘
typ ┴┴┴ └──┘ ┴ ┴└───┘ └────────┘ └──┘
doc └──┘ └───┘
377 have h2 : f.norm = 0, from (norm_zero_iff _).2 hf,
id ┴└───┘ ┴ └───────────┘ ┴ └┘
src └───┘ ┴ └───────────┘ ┴
typ ┴└───┘ ┴ └───────────┘ ┴ └┘
doc └───┘
378 by rw [h1, h2]; rw max_eq_right (norm_nonneg _)
id └┘ └┘ └──────────┘ └─────────┘
src └──┘ └┘ ┴ └─┘└──────────┘┴ └─────────┘└──┘
typ └──┘└┘└┘└┘┴ └─┘└──────────┘┴ └─────────┘└──┘
doc └──┘ └┘ ┴ └─┘ ┴ └──┘
txt └──┘ └┘ ┴ └─┘ ┴ └──┘
par └──┘ └┘ ┴ └─┘ ┴ └──┘
pid └┘ └┘ ┴ ┴ ┴ └─┘┴
st └─────┘└──┘┴└───┘└──────────┘└───────────────┘
379 else if hg : g ≈ 0 then
id └┘ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴
380 have lim_zero (g - 0), from hg,
id └──────┘ ┴ ┴ └┘
src └──────┘ ┴
typ └──────┘ ┴ ┴ └┘
doc └──────┘
381 have f + g ≈ f, from show lim_zero ((f + g) - f), by rw [add_sub_cancel']; simpa,
id ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └─────────────┘
src ┴ ┴ └──────┘ ┴ ┴ └──┘└─────────────┘┴ └───┘
typ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └──┘└─────────────┘┴ └───┘
doc └──────┘ └──┘ ┴ └───┘
txt └──┘ ┴ └───┘
par └──┘ ┴ └───┘
pid └┘ ┴
st └──────────────────┘┴└─────┘
382 have h1 : (f+g).norm = f.norm, from norm_equiv this,
id ┴┴┴ └──┘ ┴ ┴└───┘ └────────┘ └──┘
src ┴ └──┘ ┴ └───┘ └────────┘
typ ┴┴┴ └──┘ ┴ ┴└───┘ └────────┘ └──┘
doc └──┘ └───┘
383 have h2 : g.norm = 0, from (norm_zero_iff _).2 hg,
id ┴└───┘ ┴ └───────────┘ ┴ └┘
src └───┘ ┴ └───────────┘ ┴
typ ┴└───┘ ┴ └───────────┘ ┴ └┘
doc └───┘
384 by rw [h1, h2]; rw max_eq_left (norm_nonneg _)
id └┘ └┘ └─────────┘ └─────────┘
src └──┘ └┘ ┴ └─┘└─────────┘┴ └─────────┘└──┘
typ └──┘└┘└┘└┘┴ └─┘└─────────┘┴ └─────────┘└──┘
doc └──┘ └┘ ┴ └─┘ ┴ └──┘
txt └──┘ └┘ ┴ └─┘ ┴ └──┘
par └──┘ └┘ ┴ └─┘ ┴ └──┘
pid └┘ └┘ ┴ ┴ ┴ └─┘┴
st └─────┘└──┘┴└───┘└─────────┘└───────────────┘
385 else
386 begin
st └─────
387 unfold norm at ⊢ hfgne, split_ifs at ⊢ hfgne,
src └────────────────────┘ └──────────────────┘
typ └────────────────────┘ └──────────────────┘
doc └────────────────────┘ └──────────────────┘
txt └────────────────────┘ └──────────────────┘
par └────────────────────┘ └──────────────────┘
pid └───┘└─────────┘ └─────────┘
st ───────────────────────┘└────────────────────┘└─
388 padic_index_simp [hfg, hf, hg] at ⊢ hfgne,
id └─┘ └┘ └┘
src └────────────────┘ └┘ └┘ └──────────┘
typ └────────────────┘└─┘└┘└┘└┘└┘└──────────┘
doc └────────────────┘ └┘ └┘ └──────────┘
txt └────────────────┘ └┘ └┘ └──────────┘
par └────────────────┘ └┘ └┘ └──────────┘
pid └┘ └┘ └┘ ┴└─────────┘
st ──────────────────────────────────────────┘└─
389 apply padic_norm.add_eq_max_of_ne,
id └─────────────────────────┘
src └────┘└─────────────────────────┘
typ └────┘└─────────────────────────┘
doc └────┘└─────────────────────────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────────┘└─
390 simpa [hf, hg, norm] using hfgne
id └┘ └┘ └──┘ └───┘
src └─────┘ └┘ └┘└──┘└──────┘ ┴
typ └─────┘└┘└┘└┘└┘└──┘└──────┘└───┘┴
doc └─────┘ └┘ └┘└──┘└──────┘ ┴
txt └─────┘ └┘ └┘ └──────┘ ┴
par └─────┘ └┘ └┘ └──────┘ ┴
pid ┴┴ └┘ └┘ ┴┴└────┘ ┴
st ──────────────────────────────────┘
391 end
id └─┘
typ └─┘
st └─┘
392
393 end embedding
394 end padic_seq
395
396 /-- The p-adic numbers `Q_[p]` are the Cauchy completion of `ℚ` with respect to the p-adic norm. -/
397 def padic (p : ℕ) [nat.prime p] := @cau_seq.completion.Cauchy _ _ _ _ (padic_norm p) _
id ┴ └───────┘ ┴ └───────────────────────┘ └────────┘ ┴
src ┴ └───────┘ └───────────────────────┘ └────────┘
typ ┴ └───────┘ ┴ └───────────────────────┘ └────────┘ ┴
doc └───────┘ └────────┘
398 notation `ℚ_[` p `]` := padic p
id └───┘
src └───┘
typ └───┘
doc └───┘
399
400 namespace padic
401
402 section completion
403 variables {p : ℕ} [nat.prime p]
id ┴ └───────┘
src ┴ └───────┘
typ ┴ └───────┘
doc └───────┘
404
405 /-- The discrete field structure on ℚ_p is inherited from the Cauchy completion construction. -/
406 instance discrete_field : discrete_field (ℚ_[p]) :=
id └────────────┘ └─┘┴┴
src └────────────┘ └─┘ ┴
typ └────────────┘ └─┘┴┴
doc └─┘ ┴
407 cau_seq.completion.discrete_field
id └───────────────────────────────┘
src └───────────────────────────────┘
typ └───────────────────────────────┘
408
409 instance : inhabited ℚ_[p] := ⟨0⟩
id └───────┘ └─┘┴┴
src └───────┘ └─┘ ┴
typ └───────┘ └─┘┴┴
doc └─┘ ┴
410
411 -- short circuits
412
413 instance : has_zero ℚ_[p] := by apply_instance
id └──────┘ └─┘┴┴
src └──────┘ └─┘ ┴ └─────────────┘
typ └──────┘ └─┘┴┴ └─────────────┘
doc └─┘ ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
414 instance : has_one ℚ_[p] := by apply_instance
id └─────┘ └─┘┴┴
src └─────┘ └─┘ ┴ └─────────────┘
typ └─────┘ └─┘┴┴ └─────────────┘
doc └─┘ ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
415 instance : has_add ℚ_[p] := by apply_instance
id └─────┘ └─┘┴┴
src └─────┘ └─┘ ┴ └─────────────┘
typ └─────┘ └─┘┴┴ └─────────────┘
doc └─┘ ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
416 instance : has_mul ℚ_[p] := by apply_instance
id └─────┘ └─┘┴┴
src └─────┘ └─┘ ┴ └─────────────┘
typ └─────┘ └─┘┴┴ └─────────────┘
doc └─┘ ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
417 instance : has_sub ℚ_[p] := by apply_instance
id └─────┘ └─┘┴┴
src └─────┘ └─┘ ┴ └─────────────┘
typ └─────┘ └─┘┴┴ └─────────────┘
doc └─┘ ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
418 instance : has_neg ℚ_[p] := by apply_instance
id └─────┘ └─┘┴┴
src └─────┘ └─┘ ┴ └─────────────┘
typ └─────┘ └─┘┴┴ └─────────────┘
doc └─┘ ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
419 instance : has_div ℚ_[p] := by apply_instance
id └─────┘ └─┘┴┴
src └─────┘ └─┘ ┴ └─────────────┘
typ └─────┘ └─┘┴┴ └─────────────┘
doc └─┘ ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
420 instance : add_comm_group ℚ_[p] := by apply_instance
id └────────────┘ └─┘┴┴
src └────────────┘ └─┘ ┴ └─────────────┘
typ └────────────┘ └─┘┴┴ └─────────────┘
doc └─┘ ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
421 instance : comm_ring ℚ_[p] := by apply_instance
id └───────┘ └─┘┴┴
src └───────┘ └─┘ ┴ └──────────────
typ └───────┘ └─┘┴┴ └──────────────
doc └─┘ ┴ └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
422
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
423 /-- Builds the equivalence class of a Cauchy sequence of rationals. -/
424 def mk : padic_seq p → ℚ_[p] := quotient.mk
id └───────┘ ┴ └─┘┴┴ └─────────┘
src └───────┘ └─┘ ┴ └─────────┘
typ └───────┘ ┴ └─┘┴┴ └─────────┘
doc └───────┘ └─┘ ┴
425 end completion
426
427 section completion
428 variables (p : ℕ) [nat.prime p]
id ┴ └───────┘
src ┴ └───────┘
typ ┴ └───────┘
doc └───────┘
429
430 lemma mk_eq {f g : padic_seq p} : mk f = mk g ↔ f ≈ g := quotient.eq
id └───────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────────┘
src └───────┘ └┘ ┴ └┘ ┴ ┴ └─────────┘
typ └───────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────────┘
doc └───────┘ └┘ └┘
431
432 /-- Embeds the rational numbers in the p-adic numbers. -/
433 def of_rat : ℚ → ℚ_[p] := cau_seq.completion.of_rat
id ┴ └─┘┴┴ └───────────────────────┘
src ┴ └─┘ ┴ └───────────────────────┘
typ ┴ └─┘┴┴ └───────────────────────┘
doc ┴ └─┘ ┴
434
435 @[simp] lemma of_rat_add : ∀ (x y : ℚ), of_rat p (x + y) = of_rat p x + of_rat p y :=
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src ┴ └────┘ ┴ ┴ └────┘ ┴ └────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
doc └──┘ ┴ └────┘ └────┘ └────┘
436 cau_seq.completion.of_rat_add
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
437
438 @[simp] lemma of_rat_neg : ∀ (x : ℚ), of_rat p (-x) = -of_rat p x :=
id ┴ └────┘ ┴ ┴┴ ┴ ┴└────┘ ┴ ┴
src ┴ └────┘ ┴ ┴ ┴└────┘
typ ┴ └────┘ ┴ ┴┴ ┴ ┴└────┘ ┴ ┴
doc └──┘ ┴ └────┘ └────┘
439 cau_seq.completion.of_rat_neg
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
440
441 @[simp] lemma of_rat_mul : ∀ (x y : ℚ), of_rat p (x * y) = of_rat p x * of_rat p y :=
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src ┴ └────┘ ┴ ┴ └────┘ ┴ └────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
doc └──┘ ┴ └────┘ └────┘ └────┘
442 cau_seq.completion.of_rat_mul
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
443
444 @[simp] lemma of_rat_sub : ∀ (x y : ℚ), of_rat p (x - y) = of_rat p x - of_rat p y :=
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src ┴ └────┘ ┴ ┴ └────┘ ┴ └────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
doc └──┘ ┴ └────┘ └────┘ └────┘
445 cau_seq.completion.of_rat_sub
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
446
447 @[simp] lemma of_rat_div : ∀ (x y : ℚ), of_rat p (x / y) = of_rat p x / of_rat p y :=
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src ┴ └────┘ ┴ ┴ └────┘ ┴ └────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
doc └──┘ ┴ └────┘ └────┘ └────┘
448 cau_seq.completion.of_rat_div
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
449
450 @[simp] lemma of_rat_one : of_rat p 1 = 1 := rfl
id └────┘ ┴ ┴ └─┘
src └────┘ ┴ └─┘
typ └────┘ ┴ ┴ └─┘
doc └──┘ └────┘
451
452 @[simp] lemma of_rat_zero : of_rat p 0 = 0 := rfl
id └────┘ ┴ ┴ └─┘
src └────┘ ┴ └─┘
typ └────┘ ┴ ┴ └─┘
doc └──┘ └────┘
453
454 @[simp] lemma cast_eq_of_rat_of_nat (n : ℕ) : (↑n : ℚ_[p]) = of_rat p n :=
id ┴ ┴┴ └─┘┴┴ ┴ └────┘ ┴ ┴
src ┴ ┴ └─┘ ┴ ┴ └────┘
typ ┴ ┴┴ └─┘┴┴ ┴ └────┘ ┴ ┴
doc └──┘ └─┘ ┴ └────┘
455 begin
st └─────
456 induction n with n ih,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ──────────────────────┘└─
457 { refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
458 { simpa using ih }
id └┘
src └──────────┘ ┴
typ └──────────┘└┘┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st ──────────────────┘└─
459 end
st ──┘
460
461 -- without short circuits, this needs an increase of class.instance_max_depth
462 @[simp] lemma cast_eq_of_rat_of_int (n : ℤ) : ↑n = of_rat p n :=
id ┴ ┴┴ ┴ └────┘ ┴ ┴
src ┴ ┴ ┴ └────┘
typ ┴ ┴┴ ┴ └────┘ ┴ ┴
doc └──┘ └────┘
463 by induction n; simp
id ┴
src └────────┘ └────
typ └────────┘┴ └────
doc └────────┘ └────
txt └────────┘ └────
par └────────┘ └────
pid ┴ └
st └──────────────────
464
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
465 lemma cast_eq_of_rat : ∀ (q : ℚ), (↑q : ℚ_[p]) = of_rat p q
id ┴ ┴ ┴┴ └─┘┴┴ ┴ └────┘ ┴ ┴
src ┴ ┴ └─┘ ┴ ┴ └────┘
typ ┴ ┴ ┴┴ └─┘┴┴ ┴ └────┘ ┴ ┴
doc ┴ └─┘ ┴ └────┘
466 | ⟨n, d, h1, h2⟩ :=
id ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘
467 show ↑n / ↑d = _, from
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
468 have (⟨n, d, h1, h2⟩ : ℚ) = rat.mk n d, from rat.num_denom',
id ┴ ┴ └────┘ └────────────┘
src ┴ ┴ └────┘ └────────────┘
typ ┴ ┴ └────┘ └────────────┘
doc ┴ └────┘
469 by simp [this, rat.mk_eq_div, of_rat_div]
id └──┘ └───────────┘ └────────┘
src └────┘ └┘└───────────┘└┘└────────┘└─
typ └────┘└──┘└┘└───────────┘└┘└────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └───────────────────────────────────────
470
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
471 @[move_cast] lemma coe_add : ∀ {x y : ℚ}, (↑(x + y) : ℚ_[p]) = ↑x + ↑y := by simp [cast_eq_of_rat]
id ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ ┴ ┴┴ └────────────┘
src ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────┘└────────────┘└┘
typ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ ┴ ┴┴ └────┘└────────────┘└┘
doc └───────┘ ┴ └─┘ ┴ └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └─────────────────────┘
472 @[move_cast] lemma coe_neg : ∀ {x : ℚ}, (↑(-x) : ℚ_[p]) = -↑x := by simp [cast_eq_of_rat]
id ┴ ┴ ┴┴ └─┘┴┴ ┴ ┴┴┴ └────────────┘
src ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ └────┘└────────────┘└┘
typ ┴ ┴ ┴┴ └─┘┴┴ ┴ ┴┴┴ └────┘└────────────┘└┘
doc └───────┘ ┴ └─┘ ┴ └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └─────────────────────┘
473 @[move_cast] lemma coe_mul : ∀ {x y : ℚ}, (↑(x * y) : ℚ_[p]) = ↑x * ↑y := by simp [cast_eq_of_rat]
id ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ ┴ ┴┴ └────────────┘
src ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────┘└────────────┘└┘
typ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ ┴ ┴┴ └────┘└────────────┘└┘
doc └───────┘ ┴ └─┘ ┴ └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └─────────────────────┘
474 @[move_cast] lemma coe_sub : ∀ {x y : ℚ}, (↑(x - y) : ℚ_[p]) = ↑x - ↑y := by simp [cast_eq_of_rat]
id ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ ┴ ┴┴ └────────────┘
src ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────┘└────────────┘└┘
typ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ ┴ ┴┴ └────┘└────────────┘└┘
doc └───────┘ ┴ └─┘ ┴ └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └─────────────────────┘
475 @[move_cast] lemma coe_div : ∀ {x y : ℚ}, (↑(x / y) : ℚ_[p]) = ↑x / ↑y := by simp [cast_eq_of_rat]
id ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ ┴ ┴┴ └────────────┘
src ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────┘└────────────┘└─
typ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ ┴ ┴┴ └────┘└────────────┘└─
doc └───────┘ ┴ └─┘ ┴ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └──────────────────────
476
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
477 @[squash_cast] lemma coe_one : (↑1 : ℚ_[p]) = 1 := rfl
id ┴ └─┘┴┴ ┴ └─┘
src ┴ └─┘ ┴ ┴ └─┘
typ ┴ └─┘┴┴ ┴ └─┘
doc └─────────┘ └─┘ ┴
478 @[squash_cast] lemma coe_zero : (↑0 : ℚ_[p]) = 0 := rfl
id ┴ └─┘┴┴ ┴ └─┘
src ┴ └─┘ ┴ ┴ └─┘
typ ┴ └─┘┴┴ ┴ └─┘
doc └─────────┘ └─┘ ┴
479
480 lemma const_equiv {q r : ℚ} : const (padic_norm p) q ≈ const (padic_norm p) r ↔ q = r :=
id ┴ └───┘ └────────┘ ┴ ┴ ┴ └───┘ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ └────────┘ ┴ └───┘ └────────┘ ┴ ┴
typ ┴ └───┘ └────────┘ ┴ ┴ ┴ └───┘ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ └───┘ └────────┘ └───┘ └────────┘
481 ⟨ λ heq : lim_zero (const (padic_norm p) (q - r)),
id └──────┘ └───┘ └────────┘ ┴ ┴ ┴ ┴
src └──────┘ └───┘ └────────┘ ┴
typ └──────┘ └───┘ └────────┘ ┴ ┴ ┴ ┴
doc └──────┘ └───┘ └────────┘
482 eq_of_sub_eq_zero $ const_lim_zero.1 heq,
id └───────────────┘ └────────────┘┴ └─┘
src └───────────────┘ └────────────┘┴ └─┘
typ └───────────────┘ └────────────┘┴ └─┘
483 λ heq, by rw heq; apply setoid.refl _ ⟩
id └─┘ └─┘ └─────────┘
src └─┘ └─┘└─┘ └────┘└─────────┘└─┘
typ └─┘ └─┘└─┘ └────┘└─────────┘└─┘
doc └─┘ └────┘ └─┘
txt └─┘ └────┘ └─┘
par └─┘ └────┘ └─┘
pid ┴ ┴ └┘┴
st └───────────────────────────┘
484
485 lemma of_rat_eq {q r : ℚ} : of_rat p q = of_rat p r ↔ q = r :=
id ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ └────┘ ┴ ┴
typ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ └────┘ └────┘
486 ⟨(const_equiv p).1 ∘ quotient.eq.1, λ h, by rw h⟩
id └─────────┘ ┴ ┴ ┴ └─────────┘┴ ┴ ┴
src └─────────┘ ┴ ┴ └─────────┘┴ └─┘
typ └─────────┘ ┴ ┴ ┴ └─────────┘┴ ┴ └─┘┴
doc └─┘
txt └─┘
par └─┘
pid ┴
st └───┘
487
488 @[elim_cast] lemma coe_inj {q r : ℚ} : (↑q : ℚ_[p]) = ↑r ↔ q = r :=
id ┴ ┴┴ └─┘┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ └─┘┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └───────┘ ┴ └─┘ ┴
489 by simp [cast_eq_of_rat, of_rat_eq]
id └────────────┘ └───────┘
src └────┘└────────────┘└┘└───────┘└─
typ └────┘└────────────┘└┘└───────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └─────────────────────────────────
490
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
491 instance : char_zero ℚ_[p] :=
id └───────┘ └─┘┴┴
src └───────┘ └─┘ ┴
typ └───────┘ └─┘┴┴
doc └───────┘ └─┘ ┴
492 ⟨λ m n, by { rw ← rat.cast_coe_nat, norm_cast, exact id }⟩
id ┴ ┴ └──────────────┘ └┘
src └───┘└──────────────┘ └───────┘ └────┘└┘┴
typ ┴ ┴ └───┘└──────────────┘ └───────┘ └────┘└┘┴
doc └───┘ └───────┘ └────┘ ┴
txt └───┘ └───────┘ └────┘ ┴
par └───┘ └───────┘ └────┘ ┴
pid └─┘ ┴ ┴
st └──────────────────────┘└─────────┘└─────────┘└┘
493
494 end completion
495 end padic
496
497 /-- The rational-valued p-adic norm on ℚ_p is lifted from the norm on Cauchy sequences. The
498 canonical form of this function is the normed space instance, with notation `∥ ∥`. -/
499 def padic_norm_e {p : ℕ} [hp : nat.prime p] : ℚ_[p] → ℚ :=
id ┴ └───────┘ ┴ └─┘┴┴ ┴
src ┴ └───────┘ └─┘ ┴ ┴
typ ┴ └───────┘ ┴ └─┘┴┴ ┴
doc └───────┘ └─┘ ┴ ┴
500 quotient.lift padic_seq.norm $ @padic_seq.norm_equiv _ _
id └───────────┘ └────────────┘ └──────────────────┘
src └───────────┘ └────────────┘ └──────────────────┘
typ └───────────┘ └────────────┘ └──────────────────┘
doc └────────────┘
501
502 namespace padic_norm_e
503 section embedding
504 open padic_seq
505 variables {p : ℕ} [nat.prime p]
id ┴ └───────┘
src ┴ └───────┘
typ ┴ └───────┘
doc └───────┘
506
507 lemma defn (f : padic_seq p) {ε : ℚ} (hε : ε > 0) : ∃ N, ∀ i ≥ N, padic_norm_e (⟦f⟧ - f i) < ε :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └──────────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └──────────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘ ┴ └──────────┘
508 begin
st └─────
509 simp only [padic.cast_eq_of_rat],
id └──────────────────┘
src └─────────┘└──────────────────┘┴
typ └─────────┘└──────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ─────────────────────────────────┘└─
510 change ∃ N, ∀ i ≥ N, (f - const _ (f i)).norm < ε,
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src └─────┘┴└┘┴┴ └───┘ ┴ ┴┴┴└───┘└─┘ ┴ └──────┘┴┴
typ └─────┘┴└┘┴┴ └───┘ ┴ ┴┴┴└───┘└─┘ ┴┴ └──────┘┴┴┴
doc └─────┘ └┘ ┴ └───┘ ┴ ┴ ┴└───┘└─┘ ┴ └──────┘ ┴
txt └─────┘ └┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ └──────┘ ┴
par └─────┘ └┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ └──────┘ ┴
pid ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ └──────┘ ┴
st ──────────────────────────────────────────────────┘└─
511 by_contradiction h,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └┘
st ───────────────────┘└─
512 cases cauchy₂ f hε with N hN,
id └─────┘ ┴ └┘
src └────┘└─────┘┴ ┴ └────────┘
typ └────┘└─────┘┴┴┴└┘└────────┘
doc └────┘ ┴ ┴ └────────┘
txt └────┘ ┴ ┴ └────────┘
par └────┘ ┴ ┴ └────────┘
pid ┴ ┴ ┴ └────────┘
st ─────────────────────────────┘└─
513 have : ∀ N, ∃ i ≥ N, (f - const _ (f i)).norm ≥ ε,
id ┴ ┴ └───┘ ┴ ┴
src └─────┘ └┘ ┴┴└───┘ ┴┴ ┴ ┴└───┘└─┘ ┴ └──────┘ ┴
typ └─────┘ └┘ ┴┴└───┘ ┴┴ ┴ ┴└───┘└─┘ ┴┴ └──────┘ ┴┴
doc └─────┘ └┘ ┴ └───┘ ┴ ┴ ┴└───┘└─┘ ┴ └──────┘ ┴
txt └─────┘ └┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ └──────┘ ┴
par └─────┘ └┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ └──────┘ ┴
pid └───┘└┘ └┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ └──────┘ ┴
st ──────────────────────────────────────────────────┘
514 by simpa [not_forall] using h,
id └────────┘ ┴
src └─────┘└────────┘└──────┘
typ └─────┘└────────┘└──────┘┴
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └─
515 rcases this N with ⟨i, hi, hge⟩,
id └──┘ ┴
src └─────┘ ┴ └────────────────┘
typ └─────┘└──┘┴┴└────────────────┘
doc └─────┘ ┴ └────────────────┘
txt └─────┘ ┴ └────────────────┘
par └─────┘ ┴ └────────────────┘
pid ┴ ┴ └────────────────┘
st ────────────────────────────────┘└─
516 have hne : ¬ (f - const (padic_norm p) (f i)) ≈ 0,
id └───┘ └────────┘ ┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴└───┘┴ └────────┘┴ └┘ ┴ └─┘┴└┘
typ └─────────┘ ┴ ┴ ┴└───┘┴ └────────┘┴┴└┘ ┴┴┴└─┘┴└┘
doc └─────────┘ ┴ ┴ ┴└───┘┴ └────────┘┴ └┘ ┴ └─┘ └┘
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘
par └─────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘
pid └──────┘└─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴┴
st ──────────────────────────────────────────────────┘└─
517 { intro h, unfold padic_seq.norm at hge; split_ifs at hge, exact not_lt_of_ge hge hε },
id └──────────┘ └─┘ └┘
src └─────┘ └──────────────────────────┘ └──────────────┘ └────┘└──────────┘┴ ┴ ┴
typ └─────┘ └──────────────────────────┘ └──────────────┘ └────┘└──────────┘┴└─┘┴└┘┴
doc └─────┘ └──────────────────────────┘ └──────────────┘ └────┘ ┴ ┴ ┴
txt └─────┘ └──────────────────────────┘ └──────────────┘ └────┘ ┴ ┴ ┴
par └─────┘ └──────────────────────────┘ └──────────────┘ └────┘ ┴ ┴ ┴
pid └┘ └─────────────┘└─────┘ └─────┘ ┴ ┴ ┴ ┴
st ───┘└─────┘└──────────────────────────────────────────────┘└──────────────────────────┘└┘└
518 unfold padic_seq.norm at hge; split_ifs at hge,
src └──────────────────────────┘ └──────────────┘
typ └──────────────────────────┘ └──────────────┘
doc └──────────────────────────┘ └──────────────┘
txt └──────────────────────────┘ └──────────────┘
par └──────────────────────────┘ └──────────────┘
pid └─────────────┘└─────┘ └─────┘
st ───────────────────────────────────────────────┘└─
519 apply not_le_of_gt _ hge,
id └──────────┘ └─┘
src └────┘└──────────┘└─┘
typ └────┘└──────────┘└─┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ─────────────────────────┘└─
520 cases decidable.em ((stationary_point hne) ≥ N) with hgen hngen,
id └──────────┘ └──────────────┘ └─┘ ┴
src └────┘└──────────┘┴ └──────────────┘┴ └┘ ┴ └───────────────┘
typ └────┘└──────────┘┴ └──────────────┘┴└─┘└┘ ┴┴└───────────────┘
doc └────┘ ┴ └──────────────┘┴ └┘ ┴ └───────────────┘
txt └────┘ ┴ ┴ └┘ ┴ └───────────────┘
par └────┘ ┴ ┴ └┘ ┴ └───────────────┘
pid ┴ ┴ ┴ └┘ ┴ ┴└──────────────┘
st ────────────────────────────────────────────────────────────────┘└─
521 { apply hN; assumption },
src └────┘ └─────────┘
typ └────┘ └─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ ┴
st ───┘└───────────────────┘└┘└
522 { have := stationary_point_spec hne (le_refl _) (le_of_not_le hngen),
id └───────────────────┘ └─┘ └─────┘ └──────────┘ └───┘
src └──────┘└───────────────────┘┴ ┴ └─────┘└──┘ └──────────┘┴ ┴
typ └──────┘└───────────────────┘┴└─┘┴ └─────┘└──┘ └──────────┘┴└───┘┴
doc └──────┘ ┴ ┴ └──┘ ┴ ┴
txt └──────┘ ┴ ┴ └──┘ ┴ ┴
par └──────┘ ┴ ┴ └──┘ ┴ ┴
pid └───┘└─┘ ┴ ┴ └──┘ ┴ ┴
st ─────────────────────────────────────────────────────────────────────┘└─
523 rw ←this,
id └──┘
src └──┘
typ └──┘└──┘
doc └──┘
txt └──┘
par └──┘
pid └┘
st ───────────┘└─
524 apply hN,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────┘└─
525 apply le_refl, assumption }
id └─────┘
src └────┘└─────┘ └─────────┘
typ └────┘└─────┘ └─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ ┴
st ────────────────┘└───────────┘└─
526 end
st ──┘
527
528 protected lemma nonneg (q : ℚ_[p]) : padic_norm_e q ≥ 0 :=
id └─┘┴┴ └──────────┘ ┴ ┴
src └─┘ ┴ └──────────┘ ┴
typ └─┘┴┴ └──────────┘ ┴ ┴
doc └─┘ ┴ └──────────┘
529 quotient.induction_on q $ norm_nonneg
id └───────────────────┘ ┴ └─────────┘
src └───────────────────┘ └─────────┘
typ └───────────────────┘ ┴ └─────────┘
530
531 lemma zero_def : (0 : ℚ_[p]) = ⟦0⟧ := rfl
id └─┘┴┴ ┴ ┴ ┴ └─┘
src └─┘ ┴ ┴ ┴ ┴ └─┘
typ └─┘┴┴ ┴ ┴ ┴ └─┘
doc └─┘ ┴
532
533 lemma zero_iff (q : ℚ_[p]) : padic_norm_e q = 0 ↔ q = 0 :=
id └─┘┴┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──────────┘ ┴ ┴ ┴
typ └─┘┴┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └─┘ ┴ └──────────┘
534 quotient.induction_on q $
id └───────────────────┘ ┴
src └───────────────────┘
typ └───────────────────┘ ┴
535 by simpa only [zero_def, quotient.eq] using norm_zero_iff
id └──────┘ └─────────┘ └───────────┘
src └──────────┘└──────┘└┘└─────────┘└──────┘└───────────┘└
typ └──────────┘└──────┘└┘└─────────┘└──────┘└───────────┘└
doc └──────────┘ └┘ └──────┘ └
txt └──────────┘ └┘ └──────┘ └
par └──────────┘ └┘ └──────┘ └
pid ┴└──┘└┘ └┘ ┴┴└────┘ └
st └───────────────────────────────────────────────────────
536
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
537 @[simp] protected lemma zero : padic_norm_e (0 : ℚ_[p]) = 0 :=
id └──────────┘ └─┘┴┴ ┴
src └──────────┘ └─┘ ┴ ┴
typ └──────────┘ └─┘┴┴ ┴
doc └──┘ └──────────┘ └─┘ ┴
538 (zero_iff _).2 rfl
id └──────┘ ┴ └─┘
src └──────┘ ┴ └─┘
typ └──────┘ ┴ └─┘
539
540 /-- Theorems about `padic_norm_e` are named with a `'` so the names do not conflict with the
541 equivalent theorems about `norm` (`∥ ∥`). -/
542 @[simp] protected lemma one' : padic_norm_e (1 : ℚ_[p]) = 1 :=
id └──────────┘ └─┘┴┴ ┴
src └──────────┘ └─┘ ┴ ┴
typ └──────────┘ └─┘┴┴ ┴
doc └──┘ └──────────┘ └─┘ ┴
543 norm_one
id └──────┘
src └──────┘
typ └──────┘
544
545 @[simp] protected lemma neg (q : ℚ_[p]) : padic_norm_e (-q) = padic_norm_e q :=
id └─┘┴┴ └──────────┘ ┴┴ ┴ └──────────┘ ┴
src └─┘ ┴ └──────────┘ ┴ ┴ └──────────┘
typ └─┘┴┴ └──────────┘ ┴┴ ┴ └──────────┘ ┴
doc └──┘ └─┘ ┴ └──────────┘ └──────────┘
546 quotient.induction_on q $ norm_neg
id └───────────────────┘ ┴ └──────┘
src └───────────────────┘ └──────┘
typ └───────────────────┘ ┴ └──────┘
547
548 /-- Theorems about `padic_norm_e` are named with a `'` so the names do not conflict with the
549 equivalent theorems about `norm` (`∥ ∥`). -/
550 theorem nonarchimedean' (q r : ℚ_[p]) :
id └─┘┴┴
src └─┘ ┴
typ └─┘┴┴
doc └─┘ ┴
551 padic_norm_e (q + r) ≤ max (padic_norm_e q) (padic_norm_e r) :=
id └──────────┘ ┴ ┴ ┴ ┴ └─┘ └──────────┘ ┴ └──────────┘ ┴
src └──────────┘ ┴ ┴ └─┘ └──────────┘ └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ └─┘ └──────────┘ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘ └──────────┘
552 quotient.induction_on₂ q r $ norm_nonarchimedean
id └────────────────────┘ ┴ ┴ └─────────────────┘
src └────────────────────┘ └─────────────────┘
typ └────────────────────┘ ┴ ┴ └─────────────────┘
553
554 /-- Theorems about `padic_norm_e` are named with a `'` so the names do not conflict with the
555 equivalent theorems about `norm` (`∥ ∥`). -/
556 theorem add_eq_max_of_ne' {q r : ℚ_[p]} :
id └─┘┴┴
src └─┘ ┴
typ └─┘┴┴
doc └─┘ ┴
557 padic_norm_e q ≠ padic_norm_e r → padic_norm_e (q + r) = max (padic_norm_e q) (padic_norm_e r) :=
id └──────────┘ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ └─┘ └──────────┘ ┴ └──────────┘ ┴
src └──────────┘ ┴ └──────────┘ └──────────┘ ┴ ┴ └─┘ └──────────┘ └──────────┘
typ └──────────┘ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ └─┘ └──────────┘ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘ └──────────┘ └──────────┘ └──────────┘
558 quotient.induction_on₂ q r $ λ _ _, padic_seq.add_eq_max_of_ne
id └────────────────────┘ ┴ ┴ ┴ ┴ └────────────────────────┘
src └────────────────────┘ └────────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴ └────────────────────────┘
559
560 lemma triangle_ineq (x y z : ℚ_[p]) :
id └─┘┴┴
src └─┘ ┴
typ └─┘┴┴
doc └─┘ ┴
561 padic_norm_e (x - z) ≤ padic_norm_e (x - y) + padic_norm_e (y - z) :=
id └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
562 calc padic_norm_e (x - z) = padic_norm_e ((x - y) + (y - z)) : by rw sub_add_sub_cancel
id └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘
src └──────────┘ ┴ └──────────┘ ┴ ┴ ┴ └─┘└────────────────┘└
typ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└────────────────┘└
doc └──────────┘ └──────────┘ └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └──────────────────────
563 ... ≤ max (padic_norm_e (x - y)) (padic_norm_e (y - z)) : padic_norm_e.nonarchimedean' _ _
id └─┘ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────────────────────┘
src ─┘ └─┘ └──────────┘ ┴ └──────────┘ ┴ └──────────────────────────┘
typ ─┘ └─┘ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────────────────────┘
doc ─┘ └──────────┘ └──────────┘ └──────────────────────────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
564 ... ≤ padic_norm_e (x - y) + padic_norm_e (y - z) :
id └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴ ┴ └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘
565 max_le_add_of_nonneg (padic_norm_e.nonneg _) (padic_norm_e.nonneg _)
id └──────────────────┘ └─────────────────┘ └─────────────────┘
src └──────────────────┘ └─────────────────┘ └─────────────────┘
typ └──────────────────┘ └─────────────────┘ └─────────────────┘
566
567 protected lemma add (q r : ℚ_[p]) : padic_norm_e (q + r) ≤ (padic_norm_e q) + (padic_norm_e r) :=
id └─┘┴┴ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
src └─┘ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴ └──────────┘
typ └─┘┴┴ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └─┘ ┴ └──────────┘ └──────────┘ └──────────┘
568 calc
569 padic_norm_e (q + r) ≤ max (padic_norm_e q) (padic_norm_e r) : nonarchimedean' _ _
id └──────────┘ ┴ ┴ ┴ └─┘ └──────────┘ ┴ └──────────┘ ┴ └─────────────┘
src └──────────┘ ┴ └─┘ └──────────┘ └──────────┘ └─────────────┘
typ └──────────┘ ┴ ┴ ┴ └─┘ └──────────┘ ┴ └──────────┘ ┴ └─────────────┘
doc └──────────┘ └──────────┘ └──────────┘ └─────────────┘
570 ... ≤ (padic_norm_e q) + (padic_norm_e r) :
id └──────────┘ ┴ ┴ └──────────┘ ┴
src └──────────┘ ┴ └──────────┘
typ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘
571 max_le_add_of_nonneg (padic_norm_e.nonneg _) (padic_norm_e.nonneg _)
id └──────────────────┘ └─────────────────┘ └─────────────────┘
src └──────────────────┘ └─────────────────┘ └─────────────────┘
typ └──────────────────┘ └─────────────────┘ └─────────────────┘
572
573 protected lemma mul' (q r : ℚ_[p]) : padic_norm_e (q * r) = (padic_norm_e q) * (padic_norm_e r) :=
id └─┘┴┴ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
src └─┘ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴ └──────────┘
typ └─┘┴┴ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └─┘ ┴ └──────────┘ └──────────┘ └──────────┘
574 quotient.induction_on₂ q r $ norm_mul
id └────────────────────┘ ┴ ┴ └──────┘
src └────────────────────┘ └──────┘
typ └────────────────────┘ ┴ ┴ └──────┘
575
576 instance : is_absolute_value (@padic_norm_e p _) :=
id └───────────────┘ └──────────┘ ┴
src └───────────────┘ └──────────┘
typ └───────────────┘ └──────────┘ ┴
doc └───────────────┘ └──────────┘
577 { abv_nonneg := padic_norm_e.nonneg,
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
578 abv_eq_zero := zero_iff,
id └──────┘
src └──────┘
typ └──────┘
579 abv_add := padic_norm_e.add,
id └──────────────┘
src └──────────────┘
typ └──────────────┘
580 abv_mul := padic_norm_e.mul' }
id └───────────────┘
src └───────────────┘
typ └───────────────┘
581
582 @[simp] lemma eq_padic_norm' (q : ℚ) : padic_norm_e (padic.of_rat p q) = padic_norm p q :=
id ┴ └──────────┘ └──────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴
src ┴ └──────────┘ └──────────┘ ┴ └────────┘
typ ┴ └──────────┘ └──────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └──┘ ┴ └──────────┘ └──────────┘ └────────┘
583 norm_const _
id └────────┘
src └────────┘
typ └────────┘
584
585 protected theorem image' {q : ℚ_[p]} : q ≠ 0 → ∃ n : ℤ, padic_norm_e q = p ^ (-n) :=
id └─┘┴┴ ┴ ┴ ┴ ┴┴ └──────────┘ ┴ ┴ ┴ ┴ ┴┴
src └─┘ ┴ ┴ ┴ ┴┴ └──────────┘ ┴ ┴ ┴
typ └─┘┴┴ ┴ ┴ ┴ ┴┴ └──────────┘ ┴ ┴ ┴ ┴ ┴┴
doc └─┘ ┴ └──────────┘
586 quotient.induction_on q $ λ f hf,
id └───────────────────┘ ┴ ┴ └┘
src └───────────────────┘
typ └───────────────────┘ ┴ ┴ └┘
587 have ¬ f ≈ 0, from (ne_zero_iff_nequiv_zero f).1 hf,
id ┴ ┴ ┴ └─────────────────────┘ ┴ ┴ └┘
src ┴ ┴ └─────────────────────┘ ┴
typ ┴ ┴ ┴ └─────────────────────┘ ┴ ┴ └┘
588 norm_image f this
id └────────┘ ┴ └──┘
src └────────┘
typ └────────┘ ┴ └──┘
589
590 lemma sub_rev (q r : ℚ_[p]) : padic_norm_e (q - r) = padic_norm_e (r - q) :=
id └─┘┴┴ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └─┘ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
typ └─┘┴┴ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └─┘ ┴ └──────────┘ └──────────┘
591 by rw ←(padic_norm_e.neg); simp
id └──────────────┘
src └──┘ └──────────────┘┴ └────
typ └──┘ └──────────────┘┴ └────
doc └──┘ ┴ └────
txt └──┘ ┴ └────
par └──┘ ┴ └────
pid └┘ ┴ └
st └─────────────────────────────
592
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
593 end embedding
594 end padic_norm_e
595
596 namespace padic
597
598 section complete
599 open padic_seq padic
600
601 theorem rat_dense' {p : ℕ} [nat.prime p] (q : ℚ_[p]) {ε : ℚ} (hε : ε > 0) :
id ┴ └───────┘ ┴ └─┘┴┴ ┴ ┴ ┴
src ┴ └───────┘ └─┘ ┴ ┴ ┴
typ ┴ └───────┘ ┴ └─┘┴┴ ┴ ┴ ┴
doc └───────┘ └─┘ ┴ ┴
602 ∃ r : ℚ, padic_norm_e (q - r) < ε :=
id ┴ ┴┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴┴ └──────────┘ ┴ ┴
typ ┴ ┴┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc ┴ └──────────┘
603 quotient.induction_on q $ λ q',
id └───────────────────┘ ┴ └┘
src └───────────────────┘
typ └───────────────────┘ ┴ └┘
604 have ∃ N, ∀ m n ≥ N, padic_norm p (q' m - q' n) < ε, from cauchy₂ _ hε,
id ┴ ┴┴ ┴ ┴ ┴ └────────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────┘ └┘
src ┴ ┴ └────────┘ ┴ ┴ └─────┘
typ ┴ ┴┴ ┴ ┴ ┴ └────────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────┘ └┘
doc └────────┘
605 let ⟨N, hN⟩ := this in
id └─┘ ┴ └──┘
typ └─┘ ┴ └──┘
606 ⟨q' N,
id └┘
typ └┘
607 begin
st └─────
608 simp only [padic.cast_eq_of_rat],
id └──────────────────┘
src └─────────┘└──────────────────┘┴
typ └─────────┘└──────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ─────────────────────────────────────┘└─
609 change padic_seq.norm (q' - const _ (q' N)) < ε,
id └────────────┘ ┴ └───┘ └┘ ┴ ┴ ┴
src └─────┘└────────────┘┴ ┴┴┴└───┘└─┘ ┴ └─┘┴┴
typ └─────┘└────────────┘┴ ┴┴┴└───┘└─┘ └┘┴┴└─┘┴┴┴
doc └─────┘└────────────┘┴ ┴ ┴└───┘└─┘ ┴ └─┘ ┴
txt └─────┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴
par └─────┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴
pid ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴
st ────────────────────────────────────────────────────┘└─
610 cases decidable.em ((q' - const (padic_norm p) (q' N)) ≈ 0) with heq hne',
id └──────────┘ └───┘ └────────┘ ┴ └┘ ┴ ┴
src └────┘└──────────┘┴ ┴ ┴└───┘┴ └────────┘┴ └┘ ┴ └─┘┴└───────────────┘
typ └────┘└──────────┘┴ ┴ ┴└───┘┴ └────────┘┴┴└┘ └┘┴┴└─┘┴└───────────────┘
doc └────┘ ┴ ┴ ┴└───┘┴ └────────┘┴ └┘ ┴ └─┘ └───────────────┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └───────────────┘
par └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └───────────────┘
pid ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └─┘└────────────┘
st ──────────────────────────────────────────────────────────────────────────────┘└─
611 { simpa only [heq, padic_seq.norm, dif_pos] },
id └─┘ └────────────┘ └─────┘
src └──────────┘└─┘└┘└────────────┘└┘└─────┘└┘
typ └──────────┘└─┘└┘└────────────┘└┘└─────┘└┘
doc └──────────┘ └┘└────────────┘└┘ └┘
txt └──────────┘ └┘ └┘ └┘
par └──────────┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ ┴┴
st ───────┘└────────────────────────────────────────┘└┘└
612 { simp only [padic_seq.norm, dif_neg hne'],
id └────────────┘ └─────┘ └──┘
src └─────────┘└────────────┘└┘└─────┘┴ ┴
typ └─────────┘└────────────┘└┘└─────┘┴└──┘┴
doc └─────────┘└────────────┘└┘ ┴ ┴
txt └─────────┘ └┘ ┴ ┴
par └─────────┘ └┘ ┴ ┴
pid ┴└──┘└┘ └┘ ┴ ┴
st ───────────────────────────────────────────────┘└─
613 change padic_norm p (q' _ - q' _) < ε,
id └────────┘ ┴ └┘ ┴
src └─────┘└────────┘┴ ┴ └─┘ ┴ └──┘ ┴
typ └─────┘└────────┘┴┴┴ └─┘ ┴└┘└──┘ ┴┴
doc └─────┘└────────┘┴ ┴ └─┘ ┴ └──┘ ┴
txt └─────┘ ┴ ┴ └─┘ ┴ └──┘ ┴
par └─────┘ ┴ ┴ └─┘ ┴ └──┘ ┴
pid ┴ ┴ ┴ └─┘ ┴ └──┘ ┴
st ────────────────────────────────────────────┘└─
614 have := stationary_point_spec hne',
id └───────────────────┘ └──┘
src └──────┘└───────────────────┘┴
typ └──────┘└───────────────────┘┴└──┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ─────────────────────────────────────────┘└─
615 cases decidable.em (N ≥ stationary_point hne') with hle hle,
id └──────────┘ ┴ ┴ └──────────────┘ └──┘
src └────┘└──────────┘┴ ┴┴┴└──────────────┘┴ └────────────┘
typ └────┘└──────────┘┴ ┴┴┴┴└──────────────┘┴└──┘└────────────┘
doc └────┘ ┴ ┴ ┴└──────────────┘┴ └────────────┘
txt └────┘ ┴ ┴ ┴ ┴ └────────────┘
par └────┘ ┴ ┴ ┴ ┴ └────────────┘
pid ┴ ┴ ┴ ┴ ┴ ┴└───────────┘
st ──────────────────────────────────────────────────────────────────┘└─
616 { have := eq.symm (this (le_refl _) hle),
id └─────┘ └──┘ └─────┘ └─┘
src └──────┘└─────┘┴ ┴ └─────┘└──┘ ┴
typ └──────┘└─────┘┴ └──┘┴ └─────┘└──┘└─┘┴
doc └──────┘ ┴ ┴ └──┘ ┴
txt └──────┘ ┴ ┴ └──┘ ┴
par └──────┘ ┴ ┴ └──┘ ┴
pid └───┘└─┘ ┴ ┴ └──┘ ┴
st ─────────┘└────────────────────────────────────┘└─
617 simp at this, simpa [this] },
id └──┘
src └──────────┘ └─────┘ └┘
typ └──────────┘ └─────┘└──┘└┘
doc └──────────┘ └─────┘ └┘
txt └──────────┘ └─────┘ └┘
par └──────────┘ └─────┘ └┘
pid ┴└─────┘ ┴┴ ┴┴
st ─────────────────────┘└─────────────┘└┘└
618 { apply hN,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────┘└─
619 apply le_of_lt, apply lt_of_not_ge, apply hle, apply le_refl }}
id └──────┘ └──────────┘ └─────┘
src └────┘└──────┘ └────┘└──────────┘ └────┘ └────┘└─────┘┴
typ └────┘└──────┘ └────┘└──────────┘ └────┘ └────┘└─────┘┴
doc └────┘ └────┘ └────┘ └────┘ ┴
txt └────┘ └────┘ └────┘ └────┘ ┴
par └────┘ └────┘ └────┘ └────┘ ┴
pid ┴ ┴ ┴ ┴ ┴
st ───────────────────────┘└──────────────────┘└─────────┘└──────────────┘└──
620 end⟩
st ──────┘
621
622 variables {p : ℕ} [nat.prime p] (f : cau_seq _ (@padic_norm_e p _))
id ┴ └───────┘ └─────┘ └──────────┘
src ┴ └───────┘ └─────┘ └──────────┘
typ ┴ └───────┘ └─────┘ └──────────┘
doc └───────┘ └──────────┘
623 open classical
624
625 private lemma div_nat_pos (n : ℕ) : (1 / ((n + 1): ℚ)) > 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
626 div_pos zero_lt_one (by exact_mod_cast succ_pos _)
id └─────┘ └─────────┘ └──────┘
src └─────┘ └─────────┘ └─────────────┘└──────┘└┘
typ └─────┘ └─────────┘ └─────────────┘└──────┘└┘
doc └─────────────┘ └┘
txt └─────────────┘ └┘
par └─────────────┘ └┘
pid ┴ └┘
st └────────────────────────┘
627
628 def lim_seq : ℕ → ℚ := λ n, classical.some (rat_dense' (f n) (div_nat_pos n))
id ┴ ┴ ┴ └────────────┘ └────────┘ ┴ ┴ └─────────┘ ┴
src ┴ ┴ └────────────┘ └────────┘ └─────────┘
typ ┴ ┴ ┴ └────────────┘ └────────┘ ┴ ┴ └─────────┘ ┴
doc ┴
629
630 lemma exi_rat_seq_conv {ε : ℚ} (hε : 0 < ε) :
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
doc ┴
631 ∃ N, ∀ i ≥ N, padic_norm_e (f i - ((lim_seq f) i : ℚ_[p])) < ε :=
id ┴ ┴┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘┴┴ ┴ ┴
src ┴ ┴ └──────────┘ ┴ └─────┘ └─┘ ┴ ┴
typ ┴ ┴┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘┴┴ ┴ ┴
doc └──────────┘ └─┘ ┴
632 begin
st └─────
633 refine (exists_nat_gt (1/ε)).imp (λ N hN i hi, _),
id └───────────┘ ┴┴
src └─────┘ └───────────┘┴ ┴┴ └─────┘ └────────────┘
typ └─────┘ └───────────┘┴ ┴┴┴└─────┘ └────────────┘
doc └─────┘ ┴ ┴ └─────┘ └────────────┘
txt └─────┘ ┴ ┴ └─────┘ └────────────┘
par └─────┘ ┴ ┴ └─────┘ └────────────┘
pid ┴ ┴ ┴ └─────┘ └────────────┘
st ──────────────────────────────────────────────────┘└─
634 have h := classical.some_spec (rat_dense' (f i) (div_nat_pos i)),
id └─────────────────┘ └────────┘ ┴ └─────────┘ ┴
src └────────┘└─────────────────┘┴ └────────┘┴ ┴ └┘ └─────────┘┴ └┘
typ └────────┘└─────────────────┘┴ └────────┘┴ ┴┴ └┘ └─────────┘┴┴└┘
doc └────────┘ ┴ ┴ ┴ └┘ ┴ └┘
txt └────────┘ ┴ ┴ ┴ └┘ ┴ └┘
par └────────┘ ┴ ┴ ┴ └┘ ┴ └┘
pid └────┘┴└─┘ ┴ ┴ ┴ └┘ ┴ └┘
st ─────────────────────────────────────────────────────────────────┘└─
635 refine lt_of_lt_of_le h (div_le_of_le_mul (by exact_mod_cast succ_pos _) _),
id └────────────┘ ┴ └──────────────┘ └──────┘
src └─────┘└────────────┘┴ ┴ └──────────────┘┴ ┴└─────────────┘└──────┘└┘└──┘
typ └─────┘└────────────┘┴┴┴ └──────────────┘┴ └──────────────┘└──────┘└────┘
doc └─────┘ ┴ ┴ ┴ ┴└─────────────┘ └┘└──┘
txt └─────┘ ┴ ┴ ┴ ┴└─────────────┘ └┘└──┘
par └─────┘ ┴ ┴ ┴ └──────────────┘ └────┘
pid ┴ ┴ ┴ ┴ └──────────────┘ └────┘
st ──────────────────────────────────────────────┘└────────────────────────┘└──┘└─
636 rw right_distrib,
id └───────────┘
src └─┘└───────────┘
typ └─┘└───────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────┘└─
637 apply le_add_of_le_of_nonneg,
id └────────────────────┘
src └────┘└────────────────────┘
typ └────┘└────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└─
638 { exact le_mul_of_div_le hε (le_trans (le_of_lt hN) (by exact_mod_cast hi)) },
id └──────────────┘ └┘ └──────┘ └──────┘ └┘ └┘
src └────┘└──────────────┘┴ ┴ └──────┘┴ └──────┘┴ └┘ ┴└─────────────┘ └─┘
typ └────┘└──────────────┘┴└┘┴ └──────┘┴ └──────┘┴└┘└┘ └──────────────┘└┘└─┘
doc └────┘ ┴ ┴ ┴ ┴ └┘ ┴└─────────────┘ └─┘
txt └────┘ ┴ ┴ ┴ ┴ └┘ ┴└─────────────┘ └─┘
par └────┘ ┴ ┴ ┴ ┴ └┘ └──────────────┘ └─┘
pid ┴ ┴ ┴ ┴ ┴ └┘ └──────────────┘ └┘┴
st ───┘└───────────────────────────────────────────────────┘└────────────────┘└─┘└┘└
639 { apply le_of_lt, simpa }
id └──────┘
src └────┘└──────┘ └────┘
typ └────┘└──────┘ └────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st ─────────────────┘└──────┘└─
640 end
st ──┘
641
642 lemma exi_rat_seq_conv_cauchy : is_cau_seq (padic_norm p) (lim_seq f) :=
id └────────┘ └────────┘ ┴ └─────┘ ┴
src └────────┘ └────────┘ └─────┘
typ └────────┘ └────────┘ ┴ └─────┘ ┴
doc └────────┘ └────────┘
643 assume ε hε,
id ┴ └┘
typ ┴ └┘
644 have hε3 : ε / 3 > 0, from div_pos hε (by norm_num),
id ┴ ┴ ┴ └─────┘ └┘
src ┴ ┴ └─────┘ └──────┘
typ ┴ ┴ ┴ └─────┘ └┘ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st └───────┘
645 let ⟨N, hN⟩ := exi_rat_seq_conv f hε3,
id └─┘ └──────────────┘ ┴ └─┘
src └──────────────┘
typ └─┘ └──────────────┘ ┴ └─┘
646 ⟨N2, hN2⟩ := f.cauchy₂ hε3 in
id ┴└──────┘ └─┘
src └──────┘
typ ┴└──────┘ └─┘
647 begin
st └─────
648 existsi max N N2,
id └─┘ ┴ └┘
src └──────┘└─┘┴ ┴
typ └──────┘└─┘┴┴┴└┘
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────┘└─
649 intros j hj,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
650 suffices : padic_norm_e ((↑(lim_seq f j) - f (max N N2)) + (f (max N N2) - lim_seq f (max N N2))) < ε,
id └──────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴ └┘ ┴ ┴
src └─────────┘└──────────┘┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ └┘ ┴└─────┘┴ ┴ └─┘┴ ┴ └──┘┴┴
typ └─────────┘└──────────┘┴ ┴ ┴ ┴┴└┘┴┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ └┘ ┴└─────┘┴┴┴ └─┘┴┴┴└┘└──┘┴┴┴
doc └─────────┘└──────────┘┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
txt └─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
par └─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
pid └───────┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
651 { ring at this ⊢,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴└───────┘
st ───┘└────────────┘└─
652 rw [← padic_norm_e.eq_padic_norm', ← padic.cast_eq_of_rat],
id └─────────────────────────┘ └──────────────────┘
src └────┘└─────────────────────────┘└──┘└──────────────────┘┴
typ └────┘└─────────────────────────┘└──┘└──────────────────┘┴
doc └────┘ └──┘ ┴
txt └────┘ └──┘ ┴
par └────┘ └──┘ ┴
pid └──┘ └──┘ ┴
st ────────────────────────────────────┘└──────────────────────┘└──
653 exact_mod_cast this },
id └──┘
src └─────────────┘ ┴
typ └─────────────┘└──┘┴
doc └─────────────┘ ┴
txt └─────────────┘ ┴
par └─────────────┘ ┴
pid ┴ ┴
st ───────────────────────┘└┘└
654 { apply lt_of_le_of_lt,
id └────────────┘
src └────┘└────────────┘
typ └────┘└────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────┘└─
655 { apply padic_norm_e.add },
id └──────────────┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────┘└─────────────────────┘└┘└
656 { have : (3 : ℚ) ≠ 0, by norm_num,
id ┴
src └─────┘ └──┘ └┘┴└┘ └──────┘
typ └─────┘ └──┘ └┘┴└┘ └──────┘
doc └─────┘ └──┘ └┘ └┘ └──────┘
txt └─────┘ └──┘ └┘ └┘ └──────┘
par └─────┘ └──┘ └┘ └┘ └──────┘
pid └───┘└┘ └──┘ └┘ ┴┴
st ───────────────────────┘ └─
657 have : ε = ε / 3 + ε / 3 + ε / 3,
id ┴ ┴ ┴
src └─────┘ ┴┴┴ ┴┴└─┘ ┴ ┴ └─┘ ┴ ┴ └┘
typ └─────┘ ┴┴┴ ┴┴└─┘ ┴ ┴ └─┘ ┴┴┴ └┘
doc └─────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴┴
st ─────────────────────────────────────┘└─
658 { apply eq_of_mul_eq_mul_left this, simp [left_distrib, mul_div_cancel' _ this ], ring },
id └───────────────────┘ └──┘ └──────────┘ └─────────────┘ └──┘
src └────┘└───────────────────┘┴ └────┘└──────────┘└┘└─────────────┘└─┘ └┘ └───┘
typ └────┘└───────────────────┘┴└──┘ └────┘└──────────┘└┘└─────────────┘└─┘└──┘└┘ └───┘
doc └────┘ ┴ └────┘ └┘ └─┘ └┘ └───┘
txt └────┘ ┴ └────┘ └┘ └─┘ └┘ └───┘
par └────┘ ┴ └────┘ └┘ └─┘ └┘ └───┘
pid ┴ ┴ ┴┴ └┘ └─┘ └┘ ┴
st ───────┘└──────────────────────────────┘└────────────────────────────────────────────┘└─────┘└┘└
659 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────┘└─
660 apply add_lt_add,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
661 { suffices : padic_norm_e ((↑(lim_seq f j) - f j) + (f j - f (max N N2))) < ε / 3 + ε / 3,
id └──────────┘ └─────┘ ┴ ┴ └─┘ ┴ └┘ ┴
src └─────────┘└──────────┘┴ └─────┘┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘
typ └─────────┘└──────────┘┴ └─────┘┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴┴┴ ┴┴┴ └─┘┴┴┴└┘└──┘ ┴ ┴ └─┘ ┴┴┴ └┘
doc └─────────┘└──────────┘┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘
txt └─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘
par └─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘
pid └───────┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴┴
st ───────┘└─────────────────────────────────────────────────────────────────────────────────────┘
662 by simpa,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st └─
663 apply lt_of_le_of_lt,
id └────────────┘
src └────┘└────────────┘
typ └────┘└────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────┘└─
664 { apply padic_norm_e.add },
id └──────────────┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────┘└─────────────────────┘└┘└
665 { apply add_lt_add,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────┘└─
666 { rw [padic_norm_e.sub_rev],
id └──────────────────┘
src └──┘└──────────────────┘┴
typ └──┘└──────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────┘└──────────────────────┘└──
667 apply_mod_cast hN,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st ────────────────────────────┘└─
668 exact le_of_max_le_left hj },
id └───────────────┘ └┘
src └────┘└───────────────┘┴ ┴
typ └────┘└───────────────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────────────┘└┘└
669 { apply hN2,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────┘└─
670 exact le_of_max_le_right hj,
id └────────────────┘ └┘
src └────┘└────────────────┘┴
typ └────┘└────────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────────────┘└─
671 apply le_max_right }}},
id └──────────┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────┘└──┘└
672 { apply_mod_cast hN,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st ────────────────────────┘└─
673 apply le_max_left }}}
id └─────────┘
src └────┘└─────────┘┴
typ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────┘└───
674 end
st ──┘
675
676 private def lim' : padic_seq p := ⟨_, exi_rat_seq_conv_cauchy f⟩
id └───────┘ ┴ └─────────────────────┘ ┴
src └───────┘ └─────────────────────┘
typ └───────┘ ┴ └─────────────────────┘ ┴
doc └───────┘
677
678 private def lim : ℚ_[p] := ⟦lim' f⟧
id └─┘┴┴ ┴└──┘ ┴┴
src └─┘ ┴ ┴└──┘ ┴
typ └─┘┴┴ ┴└──┘ ┴┴
doc └─┘ ┴
679
680 theorem complete' : ∃ q : ℚ_[p], ∀ ε > 0, ∃ N, ∀ i ≥ N, padic_norm_e (q - f i) < ε :=
id ┴ └─┘┴┴┴ ┴ ┴ ┴┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴┴ ┴ ┴ ┴ └──────────┘ ┴ ┴
typ ┴ └─┘┴┴┴ ┴ ┴ ┴┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ ┴ └──────────┘
681 ⟨ lim f,
id └─┘ ┴
src └─┘
typ └─┘ ┴
682 λ ε hε,
id ┴ └┘
typ ┴ └┘
683 let ⟨N, hN⟩ := exi_rat_seq_conv f (show ε / 2 > 0, from div_pos hε (by norm_num)),
id └─┘ └──────────────┘ ┴ ┴ ┴ ┴ └─────┘ └┘
src └──────────────┘ ┴ ┴ └─────┘ └──────┘
typ └─┘ └──────────────┘ ┴ ┴ ┴ ┴ └─────┘ └┘ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st └───────┘
684 ⟨N2, hN2⟩ := padic_norm_e.defn (lim' f) (show ε / 2 > 0, from div_pos hε (by norm_num)) in
id └───────────────┘ └──┘ ┴ ┴ ┴ ┴ └─────┘ └┘
src └───────────────┘ └──┘ ┴ ┴ └─────┘ └──────┘
typ └───────────────┘ └──┘ ┴ ┴ ┴ ┴ └─────┘ └┘ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st └───────┘
685 begin
st └─────
686 existsi max N N2,
id └─┘ ┴ └┘
src └──────┘└─┘┴ ┴
typ └──────┘└─┘┴┴┴└┘
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────┘└─
687 intros i hi,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
688 suffices : padic_norm_e ((lim f - lim' f i) + (lim' f i - f i)) < ε,
id └──────────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └─────────┘└──────────┘┴ └─┘┴ ┴┴┴ ┴ ┴ └┘┴┴ └──┘┴ ┴ ┴ ┴ ┴ └─┘┴┴
typ └─────────┘└──────────┘┴ └─┘┴ ┴┴┴ ┴ ┴ └┘┴┴ └──┘┴ ┴ ┴ ┴┴┴┴└─┘┴┴┴
doc └─────────┘└──────────┘┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
pid └───────┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
st ──────────────────────────────────────────────────────────────────────┘└─
689 { ring at this; exact this },
id └──┘
src └──────────┘ └────┘ ┴
typ └──────────┘ └────┘└──┘┴
doc └──────────┘ └────┘ ┴
txt └──────────┘ └────┘ ┴
par └──────────┘ └────┘ ┴
pid ┴└─────┘ ┴ ┴
st ─────┘└───────────────────────┘┴
690 { apply lt_of_le_of_lt,
691 { apply padic_norm_e.add },
st ┴
692 { have : ε = ε / 2 + ε / 2, by rw ←(add_self_div_two ε); simp,
id ┴ └──────────────┘ ┴
src └──┘ └──────────────┘┴ ┴ └──┘
typ ┴ └──┘ └──────────────┘┴┴┴ └──┘
doc └──┘ ┴ ┴ └──┘
txt └──┘ ┴ ┴ └──┘
par └──┘ ┴ ┴ └──┘
pid └┘ ┴ ┴
693 rw this,
694 apply add_lt_add,
695 { apply hN2, exact le_of_max_le_right hi },
st ┴
696 { rw_mod_cast [padic_norm_e.sub_rev],
src ┴
typ ┴
doc ┴
txt ┴
par ┴
pid ┴
697 apply hN,
698 exact le_of_max_le_left hi }}}
st └───
699 end ⟩
st ────┘
700
701 end complete
702
703 section normed_space
704 variables (p : ℕ) [nat.prime p]
id ┴ └───────┘
src ┴ └───────┘
typ ┴ └───────┘
doc └───────┘
705
706 instance : has_dist ℚ_[p] := ⟨λ x y, padic_norm_e (x - y)⟩
id └──────┘ └─┘┴┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────┘ └─┘ ┴ └──────────┘ ┴
typ └──────┘ └─┘┴┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────┘ └─┘ ┴ └──────────┘
707
708 instance : metric_space ℚ_[p] :=
id └──────────┘ └─┘┴┴
src └──────────┘ └─┘ ┴
typ └──────────┘ └─┘┴┴
doc └──────────┘ └─┘ ┴
709 { dist_self := by simp [dist],
id ┴
src ┴ └────┘ ┴
typ ┴ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └──────────┘
710 dist_comm := λ x y, by unfold dist; rw ←padic_norm_e.neg (x - y); simp,
id ┴ ┴ └──────────────┘ ┴ ┴ ┴
src └─────────┘ └──┘└──────────────┘┴ ┴┴┴ ┴ └──┘
typ ┴ ┴ └─────────┘ └──┘└──────────────┘┴ ┴┴┴┴┴┴ └──┘
doc └─────────┘ └──┘ ┴ ┴ ┴ ┴ └──┘
txt └─────────┘ └──┘ ┴ ┴ ┴ ┴ └──┘
par └─────────┘ └──┘ ┴ ┴ ┴ ┴ └──┘
pid └───┘ └┘ ┴ ┴ ┴ ┴
st └──────────────────────────────────────────────┘
711 dist_triangle :=
712 begin
st └─────
713 intros, unfold dist,
src └────┘ └─────────┘
typ └────┘ └─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid └───┘
st ───────────┘└───────────┘└─
714 exact_mod_cast padic_norm_e.triangle_ineq _ _ _,
id └────────────────────────┘
src └─────────────┘└────────────────────────┘└────┘
typ └─────────────┘└────────────────────────┘└────┘
doc └─────────────┘ └────┘
txt └─────────────┘ └────┘
par └─────────────┘ └────┘
pid ┴ └────┘
st ────────────────────────────────────────────────────┘└─
715 end,
st ──────┘
716 eq_of_dist_eq_zero :=
717 begin
st └─────
718 unfold dist, intros _ _ h,
src └─────────┘ └──────────┘
typ └─────────┘ └──────────┘
doc └─────────┘ └──────────┘
txt └─────────┘ └──────────┘
par └─────────┘ └──────────┘
pid └───┘ └────┘
st ────────────────┘└────────────┘└─
719 apply eq_of_sub_eq_zero,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────┘└─
720 apply (padic_norm_e.zero_iff _).1,
id └───────────────────┘
src └────┘ └───────────────────┘└───┘
typ └────┘ └───────────────────┘└───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └─┘└┘
st ──────────────────────────────────────┘└─
721 exact_mod_cast h
id ┴
src └─────────────┘ └
typ └─────────────┘┴└
doc └─────────────┘ └
txt └─────────────┘ └
par └─────────────┘ └
pid ┴ └
st ───────────────────────
722 end }
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
723
724 instance : has_norm ℚ_[p] := ⟨λ x, padic_norm_e x⟩
id └──────┘ └─┘┴┴ ┴ └──────────┘ ┴
src └──────┘ └─┘ ┴ └──────────┘
typ └──────┘ └─┘┴┴ ┴ └──────────┘ ┴
doc └──────┘ └─┘ ┴ └──────────┘
725
726 instance : normed_field ℚ_[p] :=
id └──────────┘ └─┘┴┴
src └──────────┘ └─┘ ┴
typ └──────────┘ └─┘┴┴
doc └──────────┘ └─┘ ┴
727 { dist_eq := λ _ _, rfl,
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
728 norm_mul' := by simp [has_norm.norm, padic_norm_e.mul'] }
id └───────────────┘
src ┴ └───────────────┘
typ ┴ └───────────────┘
doc ┴
txt ┴
par ┴
st └┘ └───────────┘ └───────────────┘
729
730 instance : is_absolute_value (λ a : ℚ_[p], ∥a∥) :=
id └───────────────┘ └─┘┴┴ ┴┴┴
src └───────────────┘ └─┘ ┴ ┴ ┴
typ └───────────────┘ └─┘┴┴ ┴┴┴
doc └───────────────┘ └─┘ ┴
731 { abv_nonneg := norm_nonneg,
id └─────────┘
src └─────────┘
typ └─────────┘
732 abv_eq_zero := norm_eq_zero,
id └──────────┘
src └──────────┘
typ └──────────┘
733 abv_add := norm_add_le,
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
734 abv_mul := by simp [has_norm.norm, padic_norm_e.mul'] }
id └───────────────┘
src └───────────────┘
typ └───────────────┘
st ┴ └────┘ └─┘ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
735
736 theorem rat_dense {p : ℕ} {hp : p.prime} (q : ℚ_[p]) {ε : ℝ} (hε : ε > 0) :
id ┴ ┴└────┘ └─┘┴┴ ┴ ┴ ┴
src ┴ └────┘ └─┘ ┴ ┴ ┴
typ ┴ ┴└────┘ └─┘┴┴ ┴ ┴ ┴
doc └────┘ └─┘ ┴
737 ∃ r : ℚ, ∥q - r∥ < ε :=
id ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴
src ┴ ┴┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴
doc ┴
738 let ⟨ε', hε'l, hε'r⟩ := exists_rat_btwn hε,
id └──┘ └┘
typ └──┘ └┘
739 ⟨r, hr⟩ := rat_dense' q (by simpa using hε'l) in
id ┴ └────────┘ ┴
src └────────┘
typ ┴ └────────┘ ┴
740 ⟨r, lt.trans (by simpa [has_norm.norm] using hr) hε'r⟩
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
741
742 end normed_space
743 end padic
744
745 namespace padic_norm_e
746 section normed_space
747 variables {p : ℕ} [hp : p.prime]
id ┴ └────┘
src ┴ └────┘
typ ┴ └────┘
doc └────┘
748 include hp
749
750 @[simp] protected lemma mul (q r : ℚ_[p]) : ∥q * r∥ = ∥q∥ * ∥r∥ :=
id └─┘┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
doc └──┘ └─┘ ┴
751 by simp [has_norm.norm, padic_norm_e.mul']
st ┴
752
753 protected lemma is_norm (q : ℚ_[p]) : ↑(padic_norm_e q) = ∥q∥ := rfl
id ┴ ┴ ┴
typ ┴ ┴ ┴
754
755 theorem nonarchimedean (q r : ℚ_[p]) : ∥q + r∥ ≤ max (∥q∥) (∥r∥) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
756 begin
757 unfold has_norm.norm,
758 exact_mod_cast nonarchimedean' _ _
759 end
st └─┘
760
761 theorem add_eq_max_of_ne {q r : ℚ_[p]} (h : ∥q∥ ≠ ∥r∥) : ∥q+r∥ = max (∥q∥) (∥r∥) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
762 begin
763 unfold has_norm.norm,
764 apply_mod_cast add_eq_max_of_ne',
765 intro h',
766 apply h,
767 unfold has_norm.norm,
768 exact_mod_cast h'
769 end
st └─┘
770
771 @[simp] lemma eq_padic_norm (q : ℚ) : ∥(↑q : ℚ_[p])∥ = padic_norm p q :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
772 begin
773 unfold has_norm.norm,
774 rw [← padic_norm_e.eq_padic_norm', ← padic.cast_eq_of_rat]
st ┴
775 end
st └─┘
776
777 instance : nondiscrete_normed_field ℚ_[p] :=
id └┘ └┘ └┘ └┘ └┘ └┘ ┴
src └┘ └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘ └┘ └┘ └┘
778 { non_trivial := ⟨padic.of_rat p (p⁻¹), begin
id ┴ ┴
typ ┴ ┴
779 have h0 : p ≠ 0 := ne_of_gt (hp.pos),
id ┴
typ ┴
780 have h1 : 1 < p := hp.one_lt,
id ┴
typ ┴
781 rw [← padic.cast_eq_of_rat, eq_padic_norm],
782 simp only [padic_norm, inv_eq_zero],
id └────────┘
src └────────┘
typ └────────┘
doc └────────┘
783 simp only [if_neg] {discharger := `[exact_mod_cast h0]},
784 norm_cast,
785 simp only [padic_val_rat.inv] {discharger := `[exact_mod_cast h0]},
786 rw [neg_neg, padic_val_rat.padic_val_rat_self h1],
787 erw _root_.pow_one,
788 exact_mod_cast h1,
789 end⟩ }
st └─┘
790
791
792 protected theorem image {q : ℚ_[p]} : q ≠ 0 → ∃ n : ℤ, ∥q∥ = ↑((↑p : ℚ) ^ (-n)) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
793 quotient.induction_on q $ λ f hf,
id ┴
typ ┴
794 have ¬ f ≈ 0, from (padic_seq.ne_zero_iff_nequiv_zero f).1 hf,
id ┴
src ┴
typ ┴
795 let ⟨n, hn⟩ := padic_seq.norm_image f this in
id ┴
typ ┴
796 ⟨n, congr_arg rat.cast hn⟩
797
798 protected lemma is_rat (q : ℚ_[p]) : ∃ q' : ℚ, ∥q∥ = ↑q' :=
id ┴ ┴ ┴ └┘
src ┴
typ ┴ ┴ ┴ └┘
doc ┴
799 if h : q = 0 then ⟨0, by simp [h]⟩
800 else let ⟨n, hn⟩ := padic_norm_e.image h in ⟨_, hn⟩
801
802 def rat_norm (q : ℚ_[p]) : ℚ := classical.some (padic_norm_e.is_rat q)
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
doc ┴
803
804 lemma eq_rat_norm (q : ℚ_[p]) : ∥q∥ = rat_norm q := classical.some_spec (padic_norm_e.is_rat q)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
805
806 theorem norm_rat_le_one : ∀ {q : ℚ} (hq : ¬ p ∣ q.denom), ∥(q : ℚ_[p])∥ ≤ 1
id ┴ ┴ ┴└┘ └─┘ ┴ ┴
src ┴ └┘ └─┘
typ ┴ ┴ ┴└┘ └─┘ ┴ ┴
doc ┴
807 | ⟨n, d, hn, hd⟩ := λ hq : ¬ p ∣ d,
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
808 if hnz : n = 0 then
809 have (⟨n, d, hn, hd⟩ : ℚ) = 0,
id ┴
src ┴
typ ┴
doc ┴
810 from rat.zero_iff_num_zero.mpr hnz,
811 by norm_num [this]
812 else
813 begin
814 have hnz' : {rat . num := n, denom := d, pos := hn, cop := hd} ≠ 0, from mt rat.zero_iff_num_zero.1 hnz,
id ┴ ┴ └┘
typ ┴ ┴ └┘
815 rw [padic_norm_e.eq_padic_norm],
816 norm_cast,
817 rw [padic_norm.eq_fpow_of_nonzero p hnz', padic_val_rat_def p hnz'],
id ┴ ┴
typ ┴ ┴
818 have h : (multiplicity p d).get _ = 0, by simp [multiplicity_eq_zero_of_not_dvd, hq],
id ┴ ┴
typ ┴ ┴
819 rw_mod_cast [h, sub_zero],
820 apply fpow_le_one_of_nonpos,
821 { exact_mod_cast le_of_lt hp.one_lt, },
st └┘
822 { apply neg_nonpos_of_nonneg, norm_cast, simp, }
st └┘
823 end
824
825 lemma eq_of_norm_add_lt_right {p : ℕ} {hp : p.prime} {z1 z2 : ℚ_[p]}
id ┴ ┴└──┘ ┴
src ┴ └──┘
typ ┴ ┴└──┘ ┴
doc └──┘
826 (h : ∥z1 + z2∥ < ∥z2∥) : ∥z1∥ = ∥z2∥ :=
id └┘ ┴ └┘ └┘ ┴
typ └┘ ┴ └┘ └┘ ┴
827 by_contradiction $ λ hne,
828 not_lt_of_ge (by rw padic_norm_e.add_eq_max_of_ne hne; apply le_max_right) h
829
830 lemma eq_of_norm_add_lt_left {p : ℕ} {hp : p.prime} {z1 z2 : ℚ_[p]}
id ┴ ┴└───┘ ┴
src ┴ └───┘
typ ┴ ┴└───┘ ┴
doc └───┘
831 (h : ∥z1 + z2∥ < ∥z1∥) : ∥z1∥ = ∥z2∥ :=
id └┘ ┴ └┘ └┘ ┴
typ └┘ ┴ └┘ └┘ ┴
832 by_contradiction $ λ hne,
833 not_lt_of_ge (by rw padic_norm_e.add_eq_max_of_ne hne; apply le_max_left) h
834
835 end normed_space
836 end padic_norm_e
837
838 namespace padic
839 variables {p : ℕ} [nat.prime p]
id ┴ └──┘ └─┘
src ┴ └──┘ └─┘
typ ┴ └──┘ └─┘
doc └──┘ └─┘
840
841 set_option eqn_compiler.zeta true
doc └───────────────┘
842 instance complete : cau_seq.is_complete ℚ_[p] norm :=
id ┴
typ ┴
843 begin
844 split, intro f,
845 have cau_seq_norm_e : is_cau_seq padic_norm_e f,
846 { intros ε hε,
847 let h := is_cau f ε (by exact_mod_cast hε),
id ┴
typ ┴
848 unfold norm at h,
849 apply_mod_cast h },
st └┘
850 cases padic.complete' ⟨f, cau_seq_norm_e⟩ with q hq,
851 existsi q,
id ┴
typ ┴
852 intros ε hε,
853 cases exists_rat_btwn hε with ε' hε',
854 norm_cast at hε',
855 cases hq ε' hε'.1 with N hN, existsi N,
id └┘ ┴
typ └┘ ┴
856 intros i hi, let h := hN i hi,
id ┴ └┘
typ ┴ └┘
857 unfold norm,
858 rw_mod_cast [cau_seq.sub_apply, padic_norm_e.sub_rev],
859 refine lt.trans _ hε'.2,
860 exact_mod_cast hN i hi
id ┴ └┘
typ ┴ └┘
861 end
st └─┘
862
863 lemma padic_norm_e_lim_le {f : cau_seq ℚ_[p] norm} {a : ℝ} (ha : a > 0)
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
864 (hf : ∀ i, ∥f i∥ ≤ a) : ∥f.lim∥ ≤ a :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
865 let ⟨N, hN⟩ := setoid.symm (cau_seq.equiv_lim f) _ ha in
id ┴
typ ┴
866 calc ∥f.lim∥ = ∥f.lim - f N + f N∥ : by simp
867 ... ≤ max (∥f.lim - f N∥) (∥f N∥) : padic_norm_e.nonarchimedean _ _
868 ... ≤ a : max_le (le_of_lt (hN _ (le_refl _))) (hf _)
id ┴
typ ┴
869
870 end padic